le_iff_max'_mem — Mathlib

English

Equality of order is captured by a max'-mem condition: s ≤ t iff for every non-equality witness h, the maximal element of s Δ t belongs to t.

Русский

Равенство порядка выражается через условие max'-mem: s ≤ t эквивалентно тому, что для каждого свидетельства неравенства h максимум s Δ t принадлежит t.

LaTeX

$$$$ \\operatorname{toColex} s \\le \\operatorname{toColex} t \\iff \\forall h\\text{ with } s \\neq t, (s \\Delta t)^{\\max'}(h) \\in t $$$$

Lean4

theorem le_iff_max'_mem {s t : Colex (Finset α)} :
    s ≤ t ↔ ∀ h : s ≠ t, (ofColex s ∆ ofColex t).max' (max_mem_aux h) ∈ ofColex t :=
  toColex_le_toColex_iff_max'_mem

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