ofSet_univ_eq_refl — Mathlib

English

The identity on the whole space X, viewed as an open partial homeomorphism on Set.univ, equals the reflexive open partial homeomorphism on X.

Русский

Единичное отображение на всём пространстве X, рассмотренное как открытое частичное гомеоморфизм на Set.univ, равно тождественному открыто-полному гомеоморфизму X.

LaTeX

$$$ (\\mathrm{ofSet}(\\mathrm{Set.univ}, \\mathrm{isOpen_univ})).trans(\\mathrm{refl}~X) = \\mathrm{refl}~X $$$

Lean4

@[simp, mfld_simps]
theorem ofSet_univ_eq_refl : ofSet univ isOpen_univ = OpenPartialHomeomorph.refl X := by ext <;> simp

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