nhds_iInf — Mathlib

English

The neighborhood at a for the infimum topology iInf t is the infimum over i of the neighborhoods in t(i).

Русский

Окрестность в a для топологии iInf t равна наименьшему общему окрестностям по всем t(i).

LaTeX

$$theorem nhds_iInf {ι : Sort*} {t : ι → TopologicalSpace α} {a : α} : @nhds α (iInf t) a = ⨅ i, @nhds α (t i) a$$

Lean4

theorem nhds_iInf {ι : Sort*} {t : ι → TopologicalSpace α} {a : α} : @nhds α (iInf t) a = ⨅ i, @nhds α (t i) a :=
  (gc_nhds a).u_iInf

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