toColex_lt_toColex_iff_max'_mem — Mathlib

English

The strict Colex order is characterized by a max'-mem condition with a witness from the symmetric difference.

Русский

Строкий порядок Коэкса характеризуется по максимальному элементу через max'-mem с свидетелем из симмdiff.

LaTeX

$$$$ \\operatorname{toColex} s < \\operatorname{toColex} t \\iff \\exists hst : s \\neq t, (s \\Delta t).max' (max_mem_aux hst) \\in t $$$$

Lean4

theorem toColex_lt_toColex_iff_max'_mem :
    toColex s < toColex t ↔ ∃ hst : s ≠ t, (s ∆ t).max' (symmDiff_nonempty.2 hst) ∈ t := by
  rw [lt_iff_le_and_ne, toColex_le_toColex_iff_max'_mem]; aesop

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