ofSet_symm

Mathlib.Logic.Equiv.PartialEquiv

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

English

The inverse of the identity on s is itself.

Русский

Обратная к идентичности на s равна самой идентичности.

LaTeX

$$$(\mathrm{ofSet}(s))^{-1} = \mathrm{ofSet}(s)$$$

Lean4

@[simp, mfld_simps]
theorem ofSet_symm (s : Set α) : (PartialEquiv.ofSet s).symm = PartialEquiv.ofSet s :=
  rfl

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

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

Разделы

Аффилиация

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