nhdsWithin_Ico_eq_nhdsGE — Mathlib

English

If a < b, then the nhdsWithin of a on Ico equals the nhdsWithin on Ici: 𝓝[Ico a b] a = 𝓝[Ici a] a.

Русский

Если a < b, то окрестности внутри Ico совпадают с окрестностями сверху на Ici: 𝓝[Ico a b] a = 𝓝[Ici a] a.

LaTeX

$$$\text{(h)}\ a < b \Rightarrow 𝓝[Ico(a,b)](a) = 𝓝[Ici(a)](a).$$$

Lean4

@[simp]
theorem nhdsWithin_Ico_eq_nhdsGE (h : a < b) : 𝓝[Ico a b] a = 𝓝[≥] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iio_mem_nhds h

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