ofSet_coe

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.ofSet_coe

English

The underlying function of the identity on s is the identity function.

Русский

Базовая функция идентичности на s — тождественная функция.

LaTeX

$$$\mathrm{toFun}(\mathrm{ofSet}(s)) = \mathrm{id}$$$

Lean4

@[simp, mfld_simps]
theorem ofSet_coe (s : Set α) : (PartialEquiv.ofSet s : α → α) = id :=
  rfl

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

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

Разделы

Аффилиация

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