equiv

Mathlib.Data.Erased

URI: https://scilib.ai/kg/mathlib#Erased.equiv

English

There is a canonical equivalence between Erased α and α, i.e., Erased α ≃ α.

Русский

Существуют естественные взаимнооднозначные соответствия между Erased α и α, то есть Erased α ≃ α.

LaTeX

$$$\\text{Erased}(\\alpha) \\simeq \\alpha$$$

Lean4

/-- Equivalence between `Erased α` and `α`. -/
noncomputable def equiv (α) : Erased α ≃ α :=
  ⟨out, mk, mk_out, out_mk⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru