nhdsSet_Icc — Mathlib

English

For a ≤ b, the nhdsSet of Icc a b equals the supremum of nhds a, nhds b, and the principal of Ioo a b.

Русский

При a ≤ b, nhdsSet(Icc a b) равен верхней сумме nhds a, nhds b и принципиального фильтра на Ioo a b.

LaTeX

$$$(h : a \le b) \Rightarrow 𝓝^{s}(Icc a b) = 𝓝 a \;⊔\; 𝓝 b \;⊔\; 𝓟(Ioo(a,b))$$$

Lean4

theorem nhdsSet_Icc (h : a ≤ b) : 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b) :=
  by
  rcases h.eq_or_lt with rfl | hlt
  · simp
  · rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]

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