nhds_mono — Mathlib

English

The order of nhds agrees with the order of the filters: nhds l1 ≤ nhds l2 iff l1 ≤ l2.

Русский

Порядок окрестностей согласуется с порядком фильтров: 𝓝 l1 ≤ 𝓝 l2 ⇔ l1 ≤ l2.

LaTeX

$$$\forall {l_1 l_2 : \text{Filter}(\alpha),\; 𝓝(l_1) \le 𝓝(l_2) \iff l_1 \le l_2.$$$

Lean4

@[simp]
theorem nhds_mono {l₁ l₂ : Filter α} : 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂ :=
  by
  refine ⟨fun h => ?_, fun h => monotone_nhds h⟩
  rw [← Iic_subset_Iic, ← sInter_nhds, ← sInter_nhds]
  exact sInter_subset_sInter h

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