to_isEvenlyCovered_preimage — Mathlib

English

From an evenly covered f at x with fiber I, one obtains 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

theorem to_isEvenlyCovered_preimage {x : X} (h : IsEvenlyCovered f x I) : IsEvenlyCovered f x (f ⁻¹' { x }) :=
  h.of_fiber_homeomorph h.fiberHomeomorph

Похожие утверждения