toHomeomorphSourceTarget — Mathlib

English

For an open partial homeomorphism e and x in its source, the neighborhood filter at x equals the infimum of the comap of the neighborhood filter at e(x) and the principal filter of the source.

Русский

Для открытого частичного гомеоморфизма e и точки x из источника, фильтр соседств на x равен инфимууму фильтра coma соседств в e(x) и основной фильтр источника.

LaTeX

$$$\nhds x = \inf (comap e (nhds (e x))) (principal e.source)$$$

Lean4

/-- An open partial homeomorphism defines a homeomorphism between its source and target. -/
@[simps!]
def toHomeomorphSourceTarget : e.source ≃ₜ e.target :=
  e.homeomorphOfImageSubsetSource subset_rfl e.image_source_eq_target

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