ofSet_toPartialEquiv — Mathlib

English

The identity open partial homeomorphism on s has as its underlying partial equivalence exactly the identity on s.

Русский

Идентичный открытый частичный гомеоморфизм на s имеет в основе именно тождественное отображение на s.

LaTeX

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

Lean4

@[simp, mfld_simps]
theorem ofSet_toPartialEquiv : (ofSet s hs).toPartialEquiv = PartialEquiv.ofSet s :=
  rfl

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