image — Mathlib

English

A subset s of X is homeomorphic to its image e''s under a homeomorphism e: X ≃ₜ Y.

Русский

Подмножество s пространства X гомеоморфно своему образу e''s через гомеоморфизм e: X ≃ₜ Y.

LaTeX

$$$ s \cong_{Top} e''s,\quad x \mapsto e x. $$$

Lean4

/-- A subset of a topological space is homeomorphic to its image under a homeomorphism.
-/
@[simps!]
def image (e : X ≃ₜ Y) (s : Set X) : s ≃ₜ e '' s where
  -- TODO: by continuity!

  continuous_toFun := e.continuous.continuousOn.mapsToRestrict (mapsTo_image _ _)
  continuous_invFun := (e.symm.continuous.comp continuous_subtype_val).codRestrict _
  toEquiv := e.toEquiv.image s

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