toHomeomorph — Mathlib

English

If f: X → Y is an embedding, then X is homeomorphic to its image f(X) as a subspace of Y.

Русский

Если f: X → Y является вложением (embedding), то X гомеоморфно своему образу f(X) как подпространству Y.

LaTeX

$$$X \simeq_{\mathrm{Top}} \operatorname{range}(f).$$$

Lean4

/-- Homeomorphism given an embedding. -/
@[simps! apply_coe]
noncomputable def toHomeomorph {f : X → Y} (hf : IsEmbedding f) : X ≃ₜ Set.range f :=
  Equiv.ofInjective f hf.injective |>.toHomeomorphOfIsInducing <| IsInducing.subtypeVal.of_comp_iff.mp hf.toIsInducing

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