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]