theorem
list.rel_of_chain_cons
{α : Type u}
{R : α → α → Prop}
{a b : α}
{l : list α} :
list.chain R a (b :: l) → R a b
theorem
list.chain_of_chain_cons
{α : Type u}
{R : α → α → Prop}
{a b : α}
{l : list α} :
list.chain R a (b :: l) → list.chain R b l
theorem
list.chain.imp'
{α : Type u}
{R S : α → α → Prop}
(HRS : ∀ ⦃a b : α⦄, R a b → S a b)
{a b : α}
(Hab : ∀ ⦃c : α⦄, R a c → S b c)
{l : list α} :
list.chain R a l → list.chain S b l
theorem
list.chain.imp
{α : Type u}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b)
{a : α}
{l : list α} :
list.chain R a l → list.chain S a l
theorem
list.chain.iff
{α : Type u}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b ↔ S a b)
{a : α}
{l : list α} :
list.chain R a l ↔ list.chain S a l
theorem
list.chain.iff_mem
{α : Type u}
{R : α → α → Prop}
{a : α}
{l : list α} :
list.chain R a l ↔ list.chain (λ (x y : α), x ∈ a :: l ∧ y ∈ l ∧ R x y) a l
theorem
list.chain_singleton
{α : Type u}
{R : α → α → Prop}
{a b : α} :
list.chain R a [b] ↔ R a b
theorem
list.chain_split
{α : Type u}
{R : α → α → Prop}
{a b : α}
{l₁ l₂ : list α} :
list.chain R a (l₁ ++ b :: l₂) ↔ list.chain R a (l₁ ++ [b]) ∧ list.chain R b l₂
theorem
list.chain_map
{α : Type u}
{β : Type v}
{R : α → α → Prop}
(f : β → α)
{b : β}
{l : list β} :
list.chain R (f b) (list.map f l) ↔ list.chain (λ (a b : β), R (f a) (f b)) b l
theorem
list.chain_of_chain_map
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), S (f a) (f b) → R a b)
{a : α}
{l : list α} :
list.chain S (f a) (list.map f l) → list.chain R a l
theorem
list.chain_map_of_chain
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), R a b → S (f a) (f b))
{a : α}
{l : list α} :
list.chain R a l → list.chain S (f a) (list.map f l)
theorem
list.chain_of_pairwise
{α : Type u}
{R : α → α → Prop}
{a : α}
{l : list α} :
list.pairwise R (a :: l) → list.chain R a l
theorem
list.chain_iff_pairwise
{α : Type u}
{R : α → α → Prop}
(tr : transitive R)
{a : α}
{l : list α} :
list.chain R a l ↔ list.pairwise R (a :: l)
theorem
list.chain'.imp
{α : Type u}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b)
{l : list α} :
list.chain' R l → list.chain' S l
theorem
list.chain'.iff
{α : Type u}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b ↔ S a b)
{l : list α} :
list.chain' R l ↔ list.chain' S l
theorem
list.chain'.iff_mem
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.chain' R l ↔ list.chain' (λ (x y : α), x ∈ l ∧ y ∈ l ∧ R x y) l
@[simp]
theorem
list.chain'_split
{α : Type u}
{R : α → α → Prop}
{a : α}
{l₁ l₂ : list α} :
list.chain' R (l₁ ++ a :: l₂) ↔ list.chain' R (l₁ ++ [a]) ∧ list.chain' R (a :: l₂)
theorem
list.chain'_map
{α : Type u}
{β : Type v}
{R : α → α → Prop}
(f : β → α)
{l : list β} :
list.chain' R (list.map f l) ↔ list.chain' (λ (a b : β), R (f a) (f b)) l
theorem
list.chain'_of_chain'_map
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), S (f a) (f b) → R a b)
{l : list α} :
list.chain' S (list.map f l) → list.chain' R l
theorem
list.chain'_map_of_chain'
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), R a b → S (f a) (f b))
{l : list α} :
list.chain' R l → list.chain' S (list.map f l)
theorem
list.pairwise.chain'
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.pairwise R l → list.chain' R l
theorem
list.chain'_iff_pairwise
{α : Type u}
{R : α → α → Prop}
(tr : transitive R)
{l : list α} :
list.chain' R l ↔ list.pairwise R l
@[simp]
theorem
list.chain'_cons
{α : Type u}
{R : α → α → Prop}
{x y : α}
{l : list α} :
list.chain' R (x :: y :: l) ↔ R x y ∧ list.chain' R (y :: l)
theorem
list.chain'.cons
{α : Type u}
{R : α → α → Prop}
{x y : α}
{l : list α} :
R x y → list.chain' R (y :: l) → list.chain' R (x :: y :: l)
theorem
list.chain'.tail
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.chain' R l → list.chain' R l.tail
theorem
list.chain'.rel_head
{α : Type u}
{R : α → α → Prop}
{x y : α}
{l : list α} :
list.chain' R (x :: y :: l) → R x y
theorem
list.chain'.rel_head'
{α : Type u}
{R : α → α → Prop}
{x : α}
{l : list α}
(h : list.chain' R (x :: l))
⦃y : α⦄ :
theorem
list.chain'.cons'
{α : Type u}
{R : α → α → Prop}
{x : α}
{l : list α} :
list.chain' R l → (∀ (y : α), y ∈ l.head' → R x y) → list.chain' R (x :: l)
theorem
list.chain'_cons'
{α : Type u}
{R : α → α → Prop}
{x : α}
{l : list α} :
list.chain' R (x :: l) ↔ (∀ (y : α), y ∈ l.head' → R x y) ∧ list.chain' R l
theorem
list.chain'.append
{α : Type u}
{R : α → α → Prop}
{l₁ l₂ : list α} :
list.chain' R l₁ → list.chain' R l₂ → (∀ (x : α), x ∈ l₁.last' → ∀ (y : α), y ∈ l₂.head' → R x y) → list.chain' R (l₁ ++ l₂)
theorem
list.chain'.imp_head
{α : Type u}
{R : α → α → Prop}
{x y : α}
(h : ∀ {z : α}, R x z → R y z)
{l : list α} :
list.chain' R (x :: l) → list.chain' R (y :: l)
theorem
list.chain'_reverse
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.chain' R l.reverse ↔ list.chain' (flip R) l
theorem
list.chain'.append_overlap
{α : Type u}
{R : α → α → Prop}
{l₁ l₂ l₃ : list α} :
list.chain' R (l₁ ++ l₂) → list.chain' R (l₂ ++ l₃) → l₂ ≠ list.nil → list.chain' R (l₁ ++ l₂ ++ l₃)
If l₁ l₂ and l₃ are lists and l₁ ++ l₂ and l₂ ++ l₃ both satisfy
chain' R, then so does l₁ ++ l₂ ++ l₃ provided l₂ ≠ []
theorem
list.exists_chain_of_relation_refl_trans_gen
{α : Type u}
{r : α → α → Prop}
{a b : α} :
relation.refl_trans_gen r a b → (∃ (l : list α), list.chain r a l ∧ (a :: l).last _ = b)
If a and b are related by the reflexive transitive closure of r,
then there is a r-chain starting from a and ending on b.
theorem
list.chain.induction
{α : Type u}
{r : α → α → Prop}
(p : α → Prop)
{a b : α}
(l : list α) :
list.chain r a l → (a :: l).last _ = b → (∀ {x y : α}, r x y → p y → p x) → p b → p a
Given a chain from a to b, and a predicate true at b, if r x y → p y → p x then
the predicate is true at a.
That is, we can propagate the predicate up the chain.