Documentation

Init.Data.List.Pairwise

Lemmas about List.Pairwise and List.Nodup. #

Pairwise and Nodup #

Pairwise #

theorem List.Pairwise.sublist :
∀ {α : Type u_1} {l₁ l₂ : List α} {R : ααProp}, l₁.Sublist l₂List.Pairwise R l₂List.Pairwise R l₁
theorem List.Pairwise.imp {α : Type u_1} {R : ααProp} {S : ααProp} (H : ∀ {a b : α}, R a bS a b) {l : List α} :
theorem List.rel_of_pairwise_cons :
∀ {α : Type u_1} {a : α} {l : List α} {R : ααProp}, List.Pairwise R (a :: l)∀ {a' : α}, a' lR a a'
theorem List.Pairwise.of_cons :
∀ {α : Type u_1} {a : α} {l : List α} {R : ααProp}, List.Pairwise R (a :: l)List.Pairwise R l
theorem List.Pairwise.tail {α : Type u_1} {R : ααProp} {l : List α} (_p : List.Pairwise R l) :
List.Pairwise R l.tail
theorem List.Pairwise.imp_of_mem {α : Type u_1} {l : List α} {R : ααProp} {S : ααProp} (H : ∀ {a b : α}, a lb lR a bS a b) (p : List.Pairwise R l) :
theorem List.Pairwise.and :
∀ {α : Type u_1} {R : ααProp} {l : List α} {S : ααProp}, List.Pairwise R lList.Pairwise S lList.Pairwise (fun (a b : α) => R a b S a b) l
theorem List.pairwise_and_iff :
∀ {α : Type u_1} {R : ααProp} {l : List α} {S : ααProp}, List.Pairwise (fun (a b : α) => R a b S a b) l List.Pairwise R l List.Pairwise S l
theorem List.Pairwise.imp₂ :
∀ {α : Type u_1} {R S T : ααProp} {l : List α}, (∀ (a b : α), R a bS a bT a b)List.Pairwise R lList.Pairwise S lList.Pairwise T l
theorem List.Pairwise.iff_of_mem {α : Type u_1} {R : ααProp} {S : ααProp} {l : List α} (H : ∀ {a b : α}, a lb l(R a b S a b)) :
theorem List.Pairwise.iff {α : Type u_1} {R : ααProp} {S : ααProp} (H : ∀ (a b : α), R a b S a b) {l : List α} :
theorem List.pairwise_of_forall {α : Type u_1} {R : ααProp} {l : List α} (H : ∀ (x y : α), R x y) :
theorem List.Pairwise.and_mem {α : Type u_1} {R : ααProp} {l : List α} :
List.Pairwise R l List.Pairwise (fun (x y : α) => x l y l R x y) l
theorem List.Pairwise.imp_mem {α : Type u_1} {R : ααProp} {l : List α} :
List.Pairwise R l List.Pairwise (fun (x y : α) => x ly lR x y) l
theorem List.Pairwise.forall_of_forall_of_flip :
∀ {α : Type u_1} {l : List α} {R : ααProp}, (∀ (x : α), x lR x x)List.Pairwise R lList.Pairwise (flip R) l∀ ⦃x : α⦄, x l∀ ⦃y : α⦄, y lR x y
theorem List.pairwise_singleton {α : Type u_1} (R : ααProp) (a : α) :
theorem List.pairwise_pair {α : Type u_1} {R : ααProp} {a : α} {b : α} :
List.Pairwise R [a, b] R a b
theorem List.pairwise_map {α : Type u_1} :
∀ {α_1 : Type u_2} {f : αα_1} {R : α_1α_1Prop} {l : List α}, List.Pairwise R (List.map f l) List.Pairwise (fun (a b : α) => R (f a) (f b)) l
theorem List.Pairwise.of_map {β : Type u_1} {α : Type u_2} {R : ααProp} {l : List α} {S : ββProp} (f : αβ) (H : ∀ (a b : α), S (f a) (f b)R a b) (p : List.Pairwise S (List.map f l)) :
theorem List.Pairwise.map {β : Type u_1} {α : Type u_2} {R : ααProp} {l : List α} {S : ββProp} (f : αβ) (H : ∀ (a b : α), R a bS (f a) (f b)) (p : List.Pairwise R l) :
theorem List.pairwise_filterMap {β : Type u_1} {α : Type u_2} {R : ααProp} {f : βOption α} {l : List β} :
List.Pairwise R (List.filterMap f l) List.Pairwise (fun (a a' : β) => ∀ (b : α), b f a∀ (b' : α), b' f a'R b b') l
theorem List.Pairwise.filterMap {β : Type u_1} {α : Type u_2} {R : ααProp} {S : ββProp} (f : αOption β) (H : ∀ (a a' : α), R a a'∀ (b : β), b f a∀ (b' : β), b' f a'S b b') {l : List α} (p : List.Pairwise R l) :
@[reducible, inline, deprecated List.Pairwise.filterMap]
abbrev List.Pairwise.filter_map {β : Type u_1} {α : Type u_2} {R : ααProp} {S : ββProp} (f : αOption β) (H : ∀ (a a' : α), R a a'∀ (b : β), b f a∀ (b' : β), b' f a'S b b') {l : List α} (p : List.Pairwise R l) :
Equations
Instances For
    theorem List.pairwise_filter {α : Type u_1} {R : ααProp} {p : αProp} [DecidablePred p] {l : List α} :
    List.Pairwise R (List.filter (fun (b : α) => decide (p b)) l) List.Pairwise (fun (x y : α) => p xp yR x y) l
    theorem List.Pairwise.filter {α : Type u_1} {R : ααProp} {l : List α} (p : αBool) :
    theorem List.pairwise_append {α : Type u_1} {R : ααProp} {l₁ : List α} {l₂ : List α} :
    List.Pairwise R (l₁ ++ l₂) List.Pairwise R l₁ List.Pairwise R l₂ ∀ (a : α), a l₁∀ (b : α), b l₂R a b
    theorem List.pairwise_append_comm {α : Type u_1} {R : ααProp} (s : ∀ {x y : α}, R x yR y x) {l₁ : List α} {l₂ : List α} :
    List.Pairwise R (l₁ ++ l₂) List.Pairwise R (l₂ ++ l₁)
    theorem List.pairwise_middle {α : Type u_1} {R : ααProp} (s : ∀ {x y : α}, R x yR y x) {a : α} {l₁ : List α} {l₂ : List α} :
    List.Pairwise R (l₁ ++ a :: l₂) List.Pairwise R (a :: (l₁ ++ l₂))
    theorem List.pairwise_join {α : Type u_1} {R : ααProp} {L : List (List α)} :
    List.Pairwise R L.join (∀ (l : List α), l LList.Pairwise R l) List.Pairwise (fun (l₁ l₂ : List α) => ∀ (x : α), x l₁∀ (y : α), y l₂R x y) L
    theorem List.pairwise_bind {β : Type u_1} {α : Type u_2} {R : ββProp} {l : List α} {f : αList β} :
    List.Pairwise R (l.bind f) (∀ (a : α), a lList.Pairwise R (f a)) List.Pairwise (fun (a₁ a₂ : α) => ∀ (x : β), x f a₁∀ (y : β), y f a₂R x y) l
    theorem List.pairwise_reverse {α : Type u_1} {R : ααProp} {l : List α} :
    List.Pairwise R l.reverse List.Pairwise (fun (a b : α) => R b a) l
    @[simp]
    theorem List.pairwise_replicate {α : Type u_1} {R : ααProp} {n : Nat} {a : α} :
    theorem List.Pairwise.drop {α : Type u_1} {R : ααProp} {l : List α} {n : Nat} (h : List.Pairwise R l) :
    theorem List.Pairwise.take {α : Type u_1} {R : ααProp} {l : List α} {n : Nat} (h : List.Pairwise R l) :
    theorem List.pairwise_iff_forall_sublist :
    ∀ {α : Type u_1} {l : List α} {R : ααProp}, List.Pairwise R l ∀ {a b : α}, [a, b].Sublist lR a b
    theorem List.Pairwise.rel_of_mem_take_of_mem_drop {α : Type u_1} {R : ααProp} {n : Nat} {x : α} {y : α} {l : List α} (h : List.Pairwise R l) (hx : x List.take n l) (hy : y List.drop n l) :
    R x y
    theorem List.Pairwise.rel_of_mem_append {α : Type u_1} {R : ααProp} {x : α} {y : α} {l₁ : List α} {l₂ : List α} (h : List.Pairwise R (l₁ ++ l₂)) (hx : x l₁) (hy : y l₂) :
    R x y
    theorem List.pairwise_of_forall_mem_list {α : Type u_1} {l : List α} {r : ααProp} (h : ∀ (a : α), a l∀ (b : α), b lr a b) :
    theorem List.pairwise_pmap {β : Type u_1} {α : Type u_2} {R : ααProp} {p : βProp} {f : (b : β) → p bα} {l : List β} (h : ∀ (x : β), x lp x) :
    List.Pairwise R (List.pmap f l h) List.Pairwise (fun (b₁ b₂ : β) => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
    theorem List.Pairwise.pmap {α : Type u_1} {R : ααProp} {β : Type u_2} {l : List α} (hl : List.Pairwise R l) {p : αProp} {f : (a : α) → p aβ} (h : ∀ (x : α), x lp x) {S : ββProp} (hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x yS (f x hx) (f y hy)) :

    Nodup #

    @[simp]
    theorem List.nodup_nil {α : Type u_1} :
    [].Nodup
    @[simp]
    theorem List.nodup_cons {α : Type u_1} {a : α} {l : List α} :
    (a :: l).Nodup ¬a l l.Nodup
    theorem List.Nodup.sublist :
    ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₂.Nodupl₁.Nodup
    theorem List.Sublist.nodup :
    ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₂.Nodupl₁.Nodup
    theorem List.getElem?_inj {α : Type u_1} {i : Nat} {j : Nat} {xs : List α} (h₀ : i < xs.length) (h₁ : xs.Nodup) (h₂ : xs[i]? = xs[j]?) :
    i = j
    @[simp]
    theorem List.nodup_replicate {α : Type u_1} {n : Nat} {a : α} :
    (List.replicate n a).Nodup n 1