le_def — Mathlib

English

Colex(Finset α) is equipped with a partial order making it a well-defined Colex-ordered structure following the given le_def.

Русский

Colex(Finset α) снабжается частичным порядком, делающим его Colex-порядком согласно заданному le_def.

LaTeX

$$PartialOrder(Colex(Finset α))$$

Lean4

theorem le_def {s t : Colex (Finset α)} :
    s ≤ t ↔ ∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b :=
  Iff.rfl

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