English
The ranges of continuous local sections of a local homeomorphism form a basis for the topology on the source space.
Русский
Образы непрерывных локальных секций локального гомеоморфизма образуют базис топологии пространства-источника.
LaTeX
$$$\operatorname{IsTopologicalBasis}\left\{ U \subset X \,|\, \exists V \subset Y, \operatorname{IsOpen}(V) \wedge \exists s \in C(V,X), f \circ s = \uparrow \wedge \operatorname{range}(s) = U \right\}$$$
Lean4
/-- Ranges of continuous local sections of a local homeomorphism
form a basis of the source space. -/
theorem isTopologicalBasis (hf : IsLocalHomeomorph f) :
IsTopologicalBasis {U : Set X | ∃ V : Set Y, IsOpen V ∧ ∃ s : C(V, X), f ∘ s = (↑) ∧ Set.range s = U} :=
by
refine isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_
· rintro _ ⟨U, hU, s, hs, rfl⟩
refine (isOpenEmbedding_of_comp hf (hs ▸ ⟨IsEmbedding.subtypeVal, ?_⟩) s.continuous).isOpen_range
rwa [Subtype.range_val]
· obtain ⟨f, hxf, rfl⟩ := hf x
refine
⟨f.source ∩ U,
⟨f.target ∩ f.symm ⁻¹' U, f.symm.isOpen_inter_preimage hU,
⟨_, continuousOn_iff_continuous_restrict.mp (f.continuousOn_invFun.mono fun _ h ↦ h.1)⟩, ?_,
(Set.range_restrict _ _).trans ?_⟩,
⟨hxf, hx⟩, fun _ h ↦ h.2⟩
· ext y; exact f.right_inv y.2.1
· apply (f.symm_image_target_inter_eq _).trans
rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left f.source_preimage_target,
f.source_inter_preimage_inv_preimage]
