univ — Mathlib

English

The universal set of α is equivalent to α itself via the natural map sending an element to its value.

Русский

Единичное множество α эквивалентно самому α через естественную биекцию, отправляющую элемент на само значение.

LaTeX

$$$ \mathrm{Set.univ.Elem}(\alpha) \simeq \alpha, \quad f(x)=x, \; f^{-1}(a)=\langle a, \mathrm{trivial} \rangle. $$$

Lean4

/-- `univ α` is equivalent to `α`. -/
@[simps apply symm_apply]
protected def univ (α) : @univ α ≃ α :=
  ⟨Subtype.val, fun a => ⟨a, trivial⟩, fun ⟨_, _⟩ => rfl, fun _ => rfl⟩

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