chain_iff_pairwise — Mathlib

English

If r is transitive, then Chain r s is equivalent to r relating every pair of elements of s.

Русский

Если r транзитивно, то Chain r s эквивалентно тому, что r связано каждую пару элементов s.

LaTeX

$$$$ [IsTrans\\;\\alpha\\;r] :\\; Chain\\ r\\ s \\iff \\forall a \\in s, \\forall b \\in s, r\\ a\\ b. $$$$

Lean4

theorem chain_iff_pairwise [IsTrans α r] : Chain r s ↔ ∀ a ∈ s, ∀ b ∈ s, r a b :=
  ⟨by
    induction s with
    | nil => exact fun _ b hb ↦ (notMem_nil _ hb).elim
    | cons a l => ?_
    intro hs b hb c hc
    rw [Cycle.chain_coe_cons, List.isChain_iff_pairwise] at hs
    simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, List.not_mem_nil, IsEmpty.forall_iff,
      imp_true_iff, Pairwise.nil, forall_eq, true_and] at hs
    simp only [mem_coe_iff, mem_cons] at hb hc
    rcases hb with (rfl | hb) <;> rcases hc with (rfl | hc)
    · exact hs.1 c (Or.inr rfl)
    · exact hs.1 c (Or.inl hc)
    · exact hs.2.2 b hb
    · exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc)), Cycle.chain_of_pairwise⟩

Похожие утверждения