equivShrink — Mathlib

English

Let α be a type small in the universe w. Then there exists a bijection between α and Shrink(α); i.e. α ≃ Shrink(α).

Русский

Пусть α — тип, малый во вселенной w. Тогда существует биекция между α и Shrink(α); то есть α эквивалентен Shrink(α).

LaTeX

$$$\forall \alpha\, Small(\alpha) \Rightarrow \exists e:\alpha \cong Shrink(\alpha).$$$

Lean4

/-- The noncomputable equivalence between a `w`-small type and a model.
-/
noncomputable def equivShrink (α : Type v) [Small.{w} α] : α ≃ Shrink α :=
  Nonempty.some (Classical.choose_spec (@Small.equiv_small α _))

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