outMkEquiv — Mathlib

English

The representative of the cardinal of a type is equivalent to the original type; i.e., (|α|).out ≃ α.

Русский

Представитель кардинала типа эквивалентен самому типу; то есть (|α|).out ≃ α.

LaTeX

$$$(\\#\\alpha).out \\simeq \\alpha$$$

Lean4

/-- The representative of the cardinal of a type is equivalent to the original type. -/
def outMkEquiv {α : Type v} : (#α).out ≃ α :=
  Nonempty.some <| Cardinal.eq.mp (by simp)

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