ofSet_symm

Mathlib.Topology.OpenPartialHomeomorph

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

English

The inverse of the identity partial homeomorphism on s is again the identity on s.

Русский

Обратное к тождественному частичному гомеоморфизму на s снова является тождественным на s.

LaTeX

$$$ (\\mathrm{ofSet}(s, hs)).symm = \\mathrm{ofSet}(s, hs) $$$

Lean4

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

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

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

Разделы

Аффилиация

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