instLinearOrder — Mathlib

English

The Colex order on Finset α is a linear order; any two Colex elements are comparable.

Русский

Порядок Коэкса на Finset α является линейным: любые два элемента Коэкса сравнимы.

LaTeX

$$$$ \\text{Colex}(\\mathsf{Finset}(\\alpha)) \\text{ is a linear order} $$$$

Lean4

instance instLinearOrder : LinearOrder (Colex (Finset α))
    where
  le_total s
    t := by
    classical
    obtain rfl | hts := eq_or_ne t s
    · simp
    have ⟨a, ha, hamax⟩ := exists_max_image _ id (symmDiff_nonempty.2 <| ofColex.injective.ne_iff.2 hts)
    simp_rw [mem_symmDiff] at ha hamax
    exact
      ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
        (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)
  toDecidableLE := instDecidableLE
  toDecidableLT := instDecidableLT

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