ofSet_symm

Mathlib.Data.PEquiv

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

English

The inverse of the Set-based equivalence is itself; the operation is an involution.

Русский

Обратное частичного эквивалентного отображения, заданного множеством, равно самому отображению; операция — инволюция.

LaTeX

$$$(\\operatorname{ofSet} s).symm = \\operatorname{ofSet} s$$$

Lean4

@[simp]
theorem ofSet_symm : (ofSet s).symm = ofSet s :=
  rfl

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

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

Разделы

Аффилиация

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