toHomeomorphOfSurjective — Mathlib

English

A surjective embedding is a homeomorphism.

Русский

Сюръективное вложение является гомеоморфизмом.

LaTeX

$$$X \cong_{\mathrm{Top}} Y$$$

Lean4

/-- A surjective embedding is a homeomorphism. -/
@[simps! apply]
noncomputable def toHomeomorphOfSurjective {f : X → Y} (hf : IsEmbedding f) (hsurj : Function.Surjective f) : X ≃ₜ Y :=
  Equiv.ofBijective f ⟨hf.injective, hsurj⟩ |>.toHomeomorphOfIsInducing hf.toIsInducing

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