nhdsWithinLT_sup_nhdsWithinGE — Mathlib

English

For any a, the sup of nhdsWithin a (Iio a) and nhdsWithin a (Ici a) equals nhdsWithin a s.

Русский

Для любого a, верхняя граница nhdsWithin a (Iio a) и nhdsWithin a (Ici a) даёт nhdsWithin a s.

LaTeX

$$theorem nhdsWithinLT_sup_nhdsWithinGE (a : α) : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a$$

Lean4

theorem nhdsWithinLT_sup_nhdsWithinGE (a : α) : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a := by
  rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ici, inter_univ]

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