nhds_mono — Mathlib

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

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