English
From an evenly covered f at x with fiber I, one gets evenly covered at x with fiber f^{-1}({x}).
Русский
Из равномерно покрытого f в x с волокном I следует равномерное покрытие в x с волокном f^{-1}({x}).
LaTeX
$$$\\text{IsEvenlyCovered } f\\ x\\ I \\Rightarrow \\text{IsEvenlyCovered } f\\ x\\ (f^{-1}\\{x\\})$$$
Lean4
/-- A constructor for `IsCoveringMapOn` when there are both empty and nonempty fibers. -/
theorem mk' (F : s → Type*) [∀ x : s, TopologicalSpace (F x)] [hF : ∀ x : s, DiscreteTopology (F x)]
(t : ∀ x : s, x.1 ∈ Set.range f → { t : Trivialization (F x) f // x.1 ∈ t.baseSet })
(h : ∀ x : s, x.1 ∉ Set.range f → ∃ U ∈ 𝓝 x.1, f ⁻¹' U = ∅) : IsCoveringMapOn f s := fun x hx ↦
by
lift x to s using hx
by_cases hxf : x.1 ∈ Set.range f
· exact .to_isEvenlyCovered_preimage (.of_trivialization (t x hxf).2)
· have ⟨U, hUx, hfU⟩ := h x hxf
exact .to_isEvenlyCovered_preimage (.of_preimage_eq_empty Empty hUx hfU)
