lt_iff_max'_mem — Mathlib

English

Equivalent expression: s < t iff there exists a witness h such that the witness belongs to t and not s and no element of s not in t is not less than the witness.

Русский

Эквивалентно: s < t тогда, когда существует свидетель h, принадлежащий t и не входящий в s, и для каждого элемента из s, который не входит в t, этот элемент меньше свидетеля.

LaTeX

$$$$ \\operatorname{toColex}(s) < \\operatorname{toColex}(t) \\iff \\exists h \\in \\operatorname{Nonempty}(t \\setminus s), \\text{...} $$$$

Lean4

theorem lt_iff_max'_mem {s t : Colex (Finset α)} :
    s < t ↔ ∃ h : s ≠ t, (ofColex s ∆ ofColex t).max' (max_mem_aux h) ∈ ofColex t := by
  rw [lt_iff_le_and_ne, le_iff_max'_mem]; aesop

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