isChain — Mathlib

English

A chain closure r-closure c is a chain in the sense of the order r; i.e., there exists a chain property IsChain r c.

Русский

Замкнутое по цепочке множество является цепью в смысле порядка r; существует свойство IsChain r c.

LaTeX

$$$ \text{ChainClosure }\, r\ c \Rightarrow IsChain\, r\ c $$$

Lean4

theorem isChain (hc : ChainClosure r c) : IsChain r c := by
  induction hc with
  | succ _ h => exact h.succ
  | union hs h =>
    exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
      ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht => h t₁ ht₁ hc₁ (ht hc₂) hneq

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