chain_of_pairwise — Mathlib

English

If a relation r relates every pair of elements of s, then s forms a Chain under r.

Русский

Если связь между любыми двумя элементами множества s удовлетворяет r, то s образует цепь по отношению r.

LaTeX

$$$$ \\bigl( \\forall a \\in s, \\forall b \\in s,\\; r\\;a\\;b \\bigr) \\rightarrow Cycle.Chain\\ r\\ s. $$$$

Lean4

theorem chain_of_pairwise : (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s :=
  by
  induction s with
  | nil => exact fun _ ↦ Cycle.Chain.nil r
  | cons a l => ?_
  intro hs
  have Ha : a ∈ (a :: l : Cycle α) := by simp
  have Hl : ∀ {b} (_hb : b ∈ l), b ∈ (a :: l : Cycle α) := @fun b hb => by simp [hb]
  rw [Cycle.chain_coe_cons]
  apply Pairwise.isChain
  rw [pairwise_cons]
  refine
    ⟨fun b hb => ?_,
      pairwise_append.2
        ⟨pairwise_of_forall_mem_list fun b hb c hc => hs b (Hl hb) c (Hl hc), pairwise_singleton r a, fun b hb c hc =>
          ?_⟩⟩
  · rw [mem_append] at hb
    rcases hb with hb | hb
    · exact hs a Ha b (Hl hb)
    · rw [mem_singleton] at hb
      rw [hb]
      exact hs a Ha a Ha
  · rw [mem_singleton] at hc
    rw [hc]
    exact hs b (Hl hb) a Ha

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