singleton_le_toColex — Mathlib

English

For any finite set s, the Colex comparison of {a} with s is characterized by a being below some element of s: {a} ≤ s if and only if there exists x in s with a ≤ x.

Русский

Для любого множества s в Коэксе, {a} ≤ s эквивалентно тому, что существует элемент x ∈ s с a ≤ x.

LaTeX

$$$$ \\operatorname{toColex}({a}) \\le \\operatorname{toColex}(s) \\iff \\exists x \\in s,\\ a \\le x $$$$

Lean4

/-- `{a} ≤ s` in colex iff `s` contains an element greater than or equal to `a`. -/
theorem singleton_le_toColex : (toColex { a } : Colex (Finset α)) ≤ toColex s ↔ ∃ x ∈ s, a ≤ x := by
  simp [toColex_le_toColex]; by_cases a ∈ s <;> aesop

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