of_fiber_homeomorph — Mathlib

English

If g: I ≃ₜ J is a fiber homeomorphism, evenly covered at x with fiber I implies evenly covered at x with fiber J.

Русский

Если g: I ≃ₜ J гомеоморфно между волокнами, то равномерное покрытие сохраняется под заменой волокна.

LaTeX

$$$\\text{IsEvenlyCovered } f\\ x\\ I \\Rightarrow \\text{IsEvenlyCovered } f\\ x\\ J$$$

Lean4

theorem of_fiber_homeomorph {J} [TopologicalSpace J] (g : I ≃ₜ J) {x : X} (h : IsEvenlyCovered f x I) :
    IsEvenlyCovered f x J :=
  have ⟨inst, U, hxU, hU, hfU, H, hH⟩ := h
  ⟨g.discreteTopology, U, hxU, hU, hfU, H.trans (.prodCongr (.refl U) g), fun _ ↦ by simp [hH]⟩

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