isLocalHomeomorphOn — Mathlib

English

An OpenPartialHomeomorph is a local homeomorph on its source.

Русский

OpenPartialHomeomorph является локальным гомеоморфизмом на своей области определения.

LaTeX

$$$IsLocalHomeomorphOn\\, e\\, e.source$$$

Lean4

/-- A `OpenPartialHomeomorph` is a local homeomorphism on its source. -/
theorem isLocalHomeomorphOn (e : OpenPartialHomeomorph X Y) : IsLocalHomeomorphOn e e.source := fun _ hx ↦ ⟨e, hx, rfl⟩

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