nhdsWithinLE_sup_nhdsWithinGT — Mathlib

English

The supremum of nhdsWithin a (Iic a) and nhdsWithin a (Ioi a) equals nhdsWithin a s.

Русский

Наибольшее из nhdsWithin a (Iic a) и nhdsWithin a (Ioi a) равно nhdsWithin a s.

LaTeX

$$theorem nhdsWithinLE_sup_nhdsWithinGT (a : α) : 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s] a$$

Lean4

theorem nhdsWithinLE_sup_nhdsWithinGT (a : α) : 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s] a := by
  rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ioi, inter_univ]

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