of_preimage_eq_empty — Mathlib

English

If I is empty and there is a neighborhood U of x with f^{-1}(U) = ∅, then f evenly covers at x with fiber I.

Русский

Если волокно пустое и существует окрестность U, такая что f^{-1}(U)=∅, то f равномерно покрывает x.

LaTeX

$$$\\text{IsEvenlyCovered } f\\ x\\ I$ при $I=\\varnothing$ и $f^{-1}(U)=\\emptyset$ для окрестности U$$

Lean4

theorem of_preimage_eq_empty [IsEmpty I] {x : X} {U : Set X} (hUx : U ∈ 𝓝 x) (hfU : f ⁻¹' U = ∅) :
    IsEvenlyCovered f x I :=
  have ⟨V, hVU, hV, hxV⟩ := mem_nhds_iff.mp hUx
  have hfV : f ⁻¹' V = ∅ := Set.eq_empty_of_subset_empty ((Set.preimage_mono hVU).trans hfU.le)
  have := Set.isEmpty_coe_sort.mpr hfV
  ⟨inferInstance, _, hxV, hV, hfV ▸ isOpen_empty, .empty, isEmptyElim⟩

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