nhds_sInf — Mathlib

English

The neighborhood at a for the infimum over a set of topologies sInf s is the infimum over t in s of nhds in t.

Русский

Окрестность в a для топологии sInf s равна наименьшему общему окрестностям по всем t ∈ s.

LaTeX

$$theorem nhds_sInf {s : Set (TopologicalSpace α)} {a : α} : @nhds α (sInf s) a = ⨅ t ∈ s, @nhds α t a$$

Lean4

theorem nhds_sInf {s : Set (TopologicalSpace α)} {a : α} : @nhds α (sInf s) a = ⨅ t ∈ s, @nhds α t a :=
  (gc_nhds a).u_sInf

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