English
Let α be a type endowed with two topologies t1 and t2. Then for every a ∈ α, the neighborhood filter at a in the infimum topology t1 ⊓ t2 equals the infimum of the neighborhood filters at a in t1 and t2: nhds_{t1⊓t2}(a) = nhds_{t1}(a) ⊓ nhds_{t2}(a).
Русский
Пусть α — множество, на котором заданы две топологии t1 и t2. Тогда для любой точки a ∈ α окрестности в пересечении топологий t1 ⊓ t2 равны пересечению окрестностей в t1 и t2: nhds_{t1⊓t2}(a) = nhds_{t1}(a) ⊓ nhds_{t2}(a).
LaTeX
$$$$ \mathrm{nhds}_{t_1 \wedge t_2}(a) = \mathrm{nhds}_{t_1}(a) \wedge \mathrm{nhds}_{t_2}(a). $$$$
Lean4
theorem nhds_inf {t₁ t₂ : TopologicalSpace α} {a : α} : @nhds α (t₁ ⊓ t₂) a = @nhds α t₁ a ⊓ @nhds α t₂ a :=
(gc_nhds a).u_inf (b₁ := t₁)
