nhds_eq_inf_comap — Mathlib

English

The neighborhood of z in Z is the infimum of the comap of nhds of proj z and the comap through the fiber projection.

Русский

Окрестности z в Z равны взаимному пересечению (inf) двух образов: через proj и через проекцию волокна.

LaTeX

$$$ nhds\ z = comap\ proj\ (nhds\ (proj\ z)) \;\inf\; comap\ (Prod.snd \circ e)\ (nhds\ (e z).2) $$$

Lean4

theorem nhds_eq_inf_comap {z : Z} (hz : z ∈ e.source) :
    𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ e) (𝓝 (e z).2) :=
  by
  refine eq_of_forall_le_iff fun l ↦ ?_
  rw [le_inf_iff, ← tendsto_iff_comap, ← tendsto_iff_comap]
  exact e.tendsto_nhds_iff hz

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