English
For any open subset s of a topological space X, the identity partial homeomorphism supported on s acts as the identity on s; i.e., its domain and codomain are s and it does nothing outside s.
Русский
Пусть s — открытое подмножество пространства X. Частичный гомеоморфизм-идентичность на s обладает областью определения и областью значений равными s и совершает отображение как тождественное на s (вне s определение отсутствует).
LaTeX
$$$ (\\mathrm{ofSet}(s, hs)).toPartialEquiv = \\mathrm{PartialEquiv.ofSet}(s) $$$
Lean4
/-- The identity partial equivalence on a set `s` -/
@[simps! (attr := mfld_simps) -fullyApplied apply, simps! -isSimp source target]
def ofSet (s : Set X) (hs : IsOpen s) : OpenPartialHomeomorph X X
where
toPartialEquiv := PartialEquiv.ofSet s
open_source := hs
open_target := hs
continuousOn_toFun := continuous_id.continuousOn
continuousOn_invFun := continuous_id.continuousOn
