univ — Mathlib

English

There is an order isomorphism between Set.univ and α, i.e. between the set of all elements of α and α itself.

Русский

Существует изоморфизм порядка между Set.univ и α, то есть между множеством всех элементов α и самим α.

LaTeX

$$$\mathrm{Set.univ} \cong_o \alpha$$$

Lean4

/-- Order isomorphism between `univ : Set α` and `α`. -/
def univ : (Set.univ : Set α) ≃o α where
  toEquiv := Equiv.Set.univ α
  map_rel_iff' := Iff.rfl

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