English
If t1 ≤ t2, then the neighborhood filter at a is contained: nhds^t1 a ≤ nhds^t2 a.
Русский
Если t1 ⊆ t2, то окрестностной фильтр в a удовлетворяет nhds^{t1}(a) ⊆ nhds^{t2}(a).
LaTeX
$$theorem nhds_mono {t₁ t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) : @nhds α t₁ a ≤ @nhds α t₂ a$$
Lean4
theorem nhds_mono {t₁ t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) : @nhds α t₁ a ≤ @nhds α t₂ a :=
(gc_nhds a).monotone_u h