English
A comprehensive constructor for IsCoveringMapOn using local trivializations for each x in s.
Русский
Полный конструктор IsCoveringMapOn, использующий локальные тривиализации над каждым x∈s.
LaTeX
$$$\\text{IsCoveringMapOn } f\\ s$$$
Lean4
theorem mk (F : s → Type*) [∀ x, TopologicalSpace (F x)] [hF : ∀ x, DiscreteTopology (F x)]
(e : ∀ x, Trivialization (F x) f) (h : ∀ x, x.1 ∈ (e x).baseSet) : IsCoveringMapOn f s :=
by
cases isEmpty_or_nonempty E
· exact .of_isEmpty _ _
refine .mk' _ _ _ (fun x _ ↦ ⟨e x, h x⟩) fun x hx ↦ (hx ?_).elim
exact ⟨(e x).invFun (x, (e x <| Classical.arbitrary E).2), (e x).proj_symm_apply' (h x)⟩
