ofColex_top — Mathlib

English

The inverse of the toColex construction sends the top element back to the universe: if you start from the top and apply ofColex, you recover univ.

Русский

Обратное преобразование toColex возвращает верхнюю грань: из вершины возвращаемся к единичному множеству.

LaTeX

$$$ofColex(\top) = univ$$$

Lean4

@[simp]
theorem ofColex_top : ofColex (⊤ : Colex (Finset α)) = univ :=
  rfl

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