English
A covering map on s induces a local homeomorphism on the preimage of s.
Русский
Покрытие на s порождает локальный гомеоморфизм на прообразе s.
LaTeX
$$$\\text{IsLocalHomeomorphOn } f\\ (f^{-1}(s))$$$
Lean4
protected theorem isLocalHomeomorphOn (hf : IsCoveringMapOn f s) : IsLocalHomeomorphOn f (f ⁻¹' s) :=
by
refine IsLocalHomeomorphOn.mk f (f ⁻¹' s) fun x hx ↦ ?_
have : Nonempty (f ⁻¹' {f x}) := ⟨⟨x, rfl⟩⟩
let e := (hf (f x) hx).toTrivialization
have h := (hf (f x) hx).mem_toTrivialization_baseSet
let he := e.mem_source.2 h
refine
⟨e.toOpenPartialHomeomorph.trans
{ toFun := fun p => p.1
invFun := fun p => ⟨p, x, rfl⟩
source := e.baseSet ×ˢ ({⟨x, rfl⟩} : Set (f ⁻¹' {f x}))
target := e.baseSet
open_source := e.open_baseSet.prod (discreteTopology_iff_isOpen_singleton.1 (hf (f x) hx).1 ⟨x, rfl⟩)
open_target := e.open_baseSet
map_source' := fun p => And.left
map_target' := fun p hp => ⟨hp, rfl⟩
left_inv' := fun p hp => Prod.ext rfl hp.2.symm
right_inv' := fun p _ => rfl
continuousOn_toFun := continuousOn_fst
continuousOn_invFun := by fun_prop },
⟨he, by rwa [e.toOpenPartialHomeomorph.symm_symm, e.proj_toFun x he], (hf (f x) hx).toTrivialization_apply⟩,
fun p h => (e.proj_toFun p h.1).symm⟩
