mathlib documentation

theorem list.rel_of_pairwise_cons {α : Type u} {R : α → α → Prop} {a : α} {l : list α} (p : list.pairwise R (a :: l)) {a' : α} (a_1 : a' ∈ l) :

theorem list.pairwise_of_pairwise_cons {α : Type u} {R : α → α → Prop} {a : α} {l : list α} (p : list.pairwise R (a :: l)) :

theorem list.pairwise.imp_of_mem {α : Type u} {R S : α → α → Prop} {l : list α} (H : ∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) (p : list.pairwise R l) :

theorem list.pairwise.imp {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a b → S a b) {l : list α} (a : list.pairwise R l) :

theorem list.pairwise.and {α : Type u} {R S : α → α → Prop} {l : list α} :

theorem list.pairwise.imp₂ {α : Type u} {R S T : α → α → Prop} (H : ∀ (a b : α), R a b → S a b → T a b) {l : list α} (hR : list.pairwise R l) (hS : list.pairwise S l) :

theorem list.pairwise.iff_of_mem {α : Type u} {R S : α → α → Prop} {l : list α} (H : ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ S a b)) :

theorem list.pairwise.iff {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a b ↔ S a b) {l : list α} :

theorem list.pairwise_of_forall {α : Type u} {R : α → α → Prop} {l : list α} (H : ∀ (x y : α), R x y) :

theorem list.pairwise.and_mem {α : Type u} {R : α → α → Prop} {l : list α} :

theorem list.pairwise.imp_mem {α : Type u} {R : α → α → Prop} {l : list α} :

theorem list.pairwise_of_sublist {α : Type u} {R : α → α → Prop} {l₁ l₂ : list α} (a : l₁ <+ l₂) (a_1 : list.pairwise R l₂) :

theorem list.forall_of_forall_of_pairwise {α : Type u} {R : α → α → Prop} (H : symmetric R) {l : list α} (H₁ : ∀ (x : α), x ∈ l → R x x) (H₂ : list.pairwise R l) (x : α) (H_1 : x ∈ l) (y : α) (H_2 : y ∈ l) :

theorem list.forall_of_pairwise {α : Type u} {R : α → α → Prop} (H : symmetric R) {l : list α} (hl : list.pairwise R l) (a : α) (H_1 : a ∈ l) (b : α) (H_2 : b ∈ l) (a_1 : a ≠ b) :

theorem list.pairwise_singleton {α : Type u} (R : α → α → Prop) (a : α) :

theorem list.pairwise_pair {α : Type u} {R : α → α → Prop} {a b : α} :

theorem list.pairwise_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : list α} :

theorem list.pairwise_append_comm {α : Type u} {R : α → α → Prop} (s : symmetric R) {l₁ l₂ : list α} :

theorem list.pairwise_middle {α : Type u} {R : α → α → Prop} (s : symmetric R) {a : α} {l₁ l₂ : list α} :

theorem list.pairwise_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : list β} :

theorem list.pairwise_of_pairwise_map {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), S (f a) (f b) → R a b) {l : list α} (p : list.pairwise S (list.map f l)) :

theorem list.pairwise_map_of_pairwise {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (f a) (f b)) {l : list α} (p : list.pairwise R l) :

theorem list.pairwise_filter_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → option α) {l : list β} :

theorem list.pairwise_filter_map_of_pairwise {α : Type u} {β : Type v} {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) :

theorem list.pairwise_filter {α : Type u} {R : α → α → Prop} (p : α → Prop) [decidable_pred p] {l : list α} :

theorem list.pairwise_filter_of_pairwise {α : Type u} {R : α → α → Prop} (p : α → Prop) [decidable_pred p] {l : list α} (a : list.pairwise R l) :

theorem list.pairwise_join {α : Type u} {R : α → α → Prop} {L : list (list α)} :

theorem list.pairwise_reverse {α : Type u} {R : α → α → Prop} {l : list α} :

theorem list.pairwise_iff_nth_le {α : Type u} {R : α → α → Prop} {l : list α} :

theorem list.pairwise_sublists' {α : Type u} {R : α → α → Prop} {l : list α} (a : list.pairwise R l) :

theorem list.pairwise_sublists {α : Type u} {R : α → α → Prop} {l : list α} (H : list.pairwise R l) :

theorem list.pw_filter_nil {α : Type u} {R : α → α → Prop} [decidable_rel R] :

theorem list.pw_filter_cons_of_pos {α : Type u} {R : α → α → Prop} [decidable_rel R] {a : α} {l : list α} (h : ∀ (b : α), b ∈ list.pw_filter R l → R a b) :

theorem list.pw_filter_cons_of_neg {α : Type u} {R : α → α → Prop} [decidable_rel R] {a : α} {l : list α} (h : ¬∀ (b : α), b ∈ list.pw_filter R l → R a b) :

theorem list.pw_filter_map {α : Type u} {β : Type v} {R : α → α → Prop} [decidable_rel R] (f : β → α) (l : list β) :

theorem list.pw_filter_sublist {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :

theorem list.pw_filter_subset {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :

theorem list.pairwise_pw_filter {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :

theorem list.pw_filter_eq_self {α : Type u} {R : α → α → Prop} [decidable_rel R] {l : list α} :

theorem list.pw_filter_idempotent {α : Type u} {R : α → α → Prop} [decidable_rel R] {l : list α} :

theorem list.forall_mem_pw_filter {α : Type u} {R : α → α → Prop} [decidable_rel R] (neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z) (a : α) (l : list α) :