nhdsWithin_Icc_eq_nhdsLE — Mathlib

English

For a < b, the neighborhood filter at b relative to Icc(a,b) equals the left-neighborhood filter at b, i.e. 𝓝[Icc a b] b = 𝓝[≤] b whenever a < b.

Русский

Для a < b фильтр окрестностей в точке b, относящийся к Icc(a,b), совпадает с левым фильтром окрестностей в b: 𝓝[Icc a b] b = 𝓝[≤] b.

LaTeX

$$$ a < b \rightarrow 𝓝[Icc a b] b = 𝓝[≤] b $$$

Lean4

@[simp]
theorem nhdsWithin_Icc_eq_nhdsLE (h : a < b) : 𝓝[Icc a b] b = 𝓝[≤] b :=
  nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ici_mem_nhds h

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