nhdsWithin_Ioc_eq_nhdsLE — Mathlib

English

For a < b, the neighborhood filter at b relative to Ioc(a,b) equals the left-neighborhood filter at b: 𝓝[Ioc a b] b = 𝓝[≤] b.

Русский

Для a < b фильтр окрестностей в b относительно Ioc(a,b) равен левому фильтру окрестностей: 𝓝[Ioc a b] b = 𝓝[≤] b.

LaTeX

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

Lean4

@[simp]
theorem nhdsWithin_Ioc_eq_nhdsLE (h : a < b) : 𝓝[Ioc a b] b = 𝓝[≤] b :=
  nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ioi_mem_nhds h

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