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 (fun (x : α) => x ∈ 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 ⋯

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 = []

@[simp]

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

theorem List.getLast_pmap {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : (a : α) → p a → β) (l : List α) (hl₁ : ∀ (a : α), a ∈ l → p a) (hl₂ : l ≠ []) : (List.pmap f l hl₁).getLast ⋯ = f (l.getLast hl₂) ⋯

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, ⋯⟩) ⋯

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₂