Documentation

Init.Data.List.Attach

def List.pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (l : List α) (H : ∀ (a : α), a lP 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
Instances For
    @[implemented_by _private.Init.Data.List.Attach.0.List.attachWithImpl]
    def List.attachWith {α : Type u_1} (l : List α) (P : αProp) (H : ∀ (x : α), x lP 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
    Instances For
      @[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)
      Instances For
        @[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 lp 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 lp a} {H₂ : ∀ (a : α), a lq 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 lp 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 lp 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 lp 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 lp 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 lp 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 lp 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 lp 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 lp 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 lp 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 lp 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 lp 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₂