def List.pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (l : List α) (H : ∀ (a : α), a ∈ l → P a) : List β

O(n). Partial map. If f : Π a, P a → β is a partial function defined on a : α satisfying P, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy P, using the proof to apply f.

Equations

• List.pmap f [] x_2 = []
• List.pmap f (a :: l) H = f a ⋯ :: List.pmap f l ⋯

@[implemented_by _private.Init.Data.List.Attach.0.List.attachWithImpl]

def List.attachWith {α : Type u_1} (l : List α) (P : α → Prop) (H : ∀ (x : α), x ∈ l → P x) : List { x : α // P x }

O(1). "Attach" a proof P x that holds for all the elements of l to produce a new list with the same elements but in the type {x // P x}.

Equations

• l.attachWith P H = List.pmap Subtype.mk l H

@[inline]

def List.attach {α : Type u_1} (l : List α) : List { x : α // x ∈ l }

O(1). "Attach" the proof that the elements of l are in l to produce a new list with the same elements but in the type {x // x ∈ l}.

Equations

• l.attach = l.attachWith (Membership.mem l) ⋯

@[simp]

theorem List.attach_nil {α : Type u_1} : [].attach = []

@[simp]

theorem List.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (l : List α) (H : ∀ (a : α), a ∈ l → p a) : List.pmap (fun (a : α) (x : p a) => f a) l H = List.map f l

theorem List.pmap_congr {α : Type u_1} {β : Type u_2} {p : α → Prop} {q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (l : List α) {H₁ : ∀ (a : α), a ∈ l → p a} {H₂ : ∀ (a : α), a ∈ l → q a} (h : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) : List.pmap f l H₁ = List.pmap g l H₂

theorem List.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (l : List α) (H : ∀ (a : α), a ∈ l → p a) : List.map g (List.pmap f l H) = List.pmap (fun (a : α) (h : p a) => g (f a h)) l H

theorem List.pmap_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : β → Prop} (g : (b : β) → p b → γ) (f : α → β) (l : List α) (H : ∀ (a : β), a ∈ List.map f l → p a) : List.pmap g (List.map f l) H = List.pmap (fun (a : α) (h : p (f a)) => g (f a) h) l ⋯

@[simp]

theorem List.attach_cons {α : Type u_1} (x : α) (xs : List α) : (x :: xs).attach = ⟨x, ⋯⟩ :: List.map (fun (x_1 : { x : α // x ∈ xs }) => match x_1 with | ⟨y, h⟩ => ⟨y, ⋯⟩) xs.attach

theorem List.pmap_eq_map_attach {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (l : List α) (H : ∀ (a : α), a ∈ l → p a) : List.pmap f l H = List.map (fun (x : { x : α // x ∈ l }) => f x.val ⋯) l.attach

theorem List.attach_map_coe {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) : List.map (fun (i : { i : α // i ∈ l }) => f i.val) l.attach = List.map f l

theorem List.attach_map_val {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) : List.map (fun (i : { x : α // x ∈ l }) => f i.val) l.attach = List.map f l

@[simp]

theorem List.attach_map_subtype_val {α : Type u_1} (l : List α) : List.map Subtype.val l.attach = l

theorem List.countP_attach {α : Type u_1} (l : List α) (p : α → Bool) : List.countP (fun (a : { x : α // x ∈ l }) => p a.val) l.attach = List.countP p l

@[simp]

theorem List.count_attach {α : Type u_1} [DecidableEq α] (l : List α) (a : { x : α // x ∈ l }) : List.count a l.attach = List.count a.val l

@[simp]

theorem List.mem_attach {α : Type u_1} (l : List α) (x : { x : α // x ∈ l }) : x ∈ l.attach

@[simp]

theorem List.mem_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ (a : α), a ∈ l → p a} {b : β} : b ∈ List.pmap f l H ↔ ∃ (a : α), ∃ (h : a ∈ l), f a ⋯ = b

@[simp]

theorem List.length_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ (a : α), a ∈ l → p a} : (List.pmap f l H).length = l.length

@[simp]

theorem List.length_attach {α : Type u_1} (L : List α) : L.attach.length = L.length

@[simp]

theorem List.pmap_eq_nil {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ (a : α), a ∈ l → p a} : List.pmap f l H = [] ↔ l = []

theorem List.pmap_ne_nil {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs → P a) : List.pmap f xs H ≠ [] ↔ xs ≠ []

@[simp]

theorem List.attach_eq_nil {α : Type u_1} (l : List α) : l.attach = [] ↔ l = []

theorem List.getElem?_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (h : ∀ (a : α), a ∈ l → p a) (n : Nat) : (List.pmap f l h)[n]? = Option.pmap f l[n]? ⋯

theorem List.get?_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (h : ∀ (a : α), a ∈ l → p a) (n : Nat) : (List.pmap f l h).get? n = Option.pmap f (l.get? n) ⋯

theorem List.getElem_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (h : ∀ (a : α), a ∈ l → p a) {n : Nat} (hn : n < (List.pmap f l h).length) : (List.pmap f l h)[n] = f l[n] ⋯

theorem List.get_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (h : ∀ (a : α), a ∈ l → p a) {n : Nat} (hn : n < (List.pmap f l h).length) : (List.pmap f l h).get ⟨n, hn⟩ = f (l.get ⟨n, ⋯⟩) ⋯

@[simp]

theorem List.head?_pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs → P a) : (List.pmap f xs H).head? = Option.map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨a, m⟩ => f a ⋯) xs.attach.head?

@[simp]

theorem List.head_pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs → P a) (h : List.pmap f xs H ≠ []) : (List.pmap f xs H).head h = f (xs.head ⋯) ⋯

@[simp]

theorem List.pmap_append {ι : Type u_1} {α : Type u_2} {p : ι → Prop} (f : (a : ι) → p a → α) (l₁ : List ι) (l₂ : List ι) (h : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a) : List.pmap f (l₁ ++ l₂) h = List.pmap f l₁ ⋯ ++ List.pmap f l₂ ⋯

theorem List.pmap_append' {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (l₁ : List α) (l₂ : List α) (h₁ : ∀ (a : α), a ∈ l₁ → p a) (h₂ : ∀ (a : α), a ∈ l₂ → p a) : List.pmap f (l₁ ++ l₂) ⋯ = List.pmap f l₁ h₁ ++ List.pmap f l₂ h₂

@[simp]

theorem List.pmap_reverse {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs.reverse → P a) : List.pmap f xs.reverse H = (List.pmap f xs ⋯).reverse

theorem List.reverse_pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs → P a) : (List.pmap f xs H).reverse = List.pmap f xs.reverse ⋯

@[simp]

theorem List.attach_append {α : Type u_1} (xs : List α) (ys : List α) : (xs ++ ys).attach = List.map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach ++ List.map (fun (x : { x : α // x ∈ ys }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) ys.attach

@[simp]

theorem List.attach_reverse {α : Type u_1} (xs : List α) : xs.reverse.attach = List.map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach.reverse

theorem List.reverse_attach {α : Type u_1} (xs : List α) : xs.attach.reverse = List.map (fun (x : { x : α // x ∈ xs.reverse }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.reverse.attach

theorem List.getLast?_attach {α : Type u_1} {xs : List α} : xs.attach.getLast? = match h : xs.getLast? with | none => none | some a => some ⟨a, ⋯⟩

@[simp]

theorem List.getLast?_pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs → P a) : (List.pmap f xs H).getLast? = Option.map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨a, m⟩ => f a ⋯) xs.attach.getLast?

@[simp]

theorem List.getLast_pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs → P a) (h : List.pmap f xs H ≠ []) : (List.pmap f xs H).getLast h = f (xs.getLast ⋯) ⋯