toPEquiv_refl

Mathlib.Data.PEquiv

URI: https://scilib.ai/kg/mathlib#Equiv.toPEquiv_refl

English

The identity Equiv maps to the identity partial equivalence.

Русский

Тождественный эквивалент преобразуется в тождественное частичное эквивалентное отображение.

LaTeX

$$$(Equiv.refl α).toPEquiv = PEquiv.refl α$$$

Lean4

@[simp]
theorem toPEquiv_refl : (Equiv.refl α).toPEquiv = PEquiv.refl α :=
  rfl

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

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

Разделы

Аффилиация

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