English
If x is evenly covered by f with fiber I, then I is homeomorphic to the fiber f^{-1}({x}).
Русский
Если точка x равномерно покрыта отображением f: E→X с волокном I, то I гомеоморфна к волокну f^{-1}({x}).
LaTeX
$$$I \\cong_{\\mathrm{top}} f^{-1}(\{x\\})$$$
Lean4
/-- A point `x : X` is evenly covered by `f : E → X` if `x` has an evenly covered neighborhood.
**Remark**: `DiscreteTopology I ∧ ∃ Trivialization I f, x ∈ t.baseSet` would be a simpler
definition, but unfortunately it does not work if `E` is nonempty but nonetheless `f` has empty
fibers over `s`. If `OpenPartialHomeomorph` could be refactored to work with an empty space and a
nonempty space while preserving the APIs, we could switch back to the definition. -/
def IsEvenlyCovered (x : X) (I : Type*) [TopologicalSpace I] :=
DiscreteTopology I ∧ ∃ U : Set X, x ∈ U ∧ IsOpen U ∧ IsOpen (f ⁻¹' U) ∧ ∃ H : f ⁻¹' U ≃ₜ U × I, ∀ x, (H x).1.1 = f x
