total — Mathlib

English

For any two ChainClosure r-closed sets c1 and c2, either c1 is contained in c2 or c2 is contained in c1; the family of chain closures is totally ordered by inclusion.

Русский

Для любых двух цепочных замкнутых множеств c1 и c2, либо c1 ⊆ c2, либо c2 ⊆ c1; семейство ChainClosure упорядочено по включению.

LaTeX

$$$ \text{ChainClosure}\, r\ c_{1} \to \text{ChainClosure}\, r\ c_{2} \Rightarrow c_{1} \subseteq c_{2} \lor c_{2} \subseteq c_{1} $$$

Lean4

theorem total (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) : c₁ ⊆ c₂ ∨ c₂ ⊆ c₁ :=
  ((chainClosure_succ_total_aux hc₂) fun _ hc₃ => chainClosure_succ_total hc₃ hc₁).imp_left subset_succChain.trans

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