Ico_mem_nhdsGE — Mathlib

English

If a < b in a linearly ordered space with ClosedIciTopology, then the half-open interval Ico(a,b) is a neighborhood of a from above: Ico(a,b) ∈ 𝓝[≥] a.

Русский

Если a < b, то полузакрытый интервал Ico(a,b) является окрестностью сверху точки a: Ico(a,b) ∈ 𝓝[≥] a.

LaTeX

$$$\forall a,b\, (a < b) \Rightarrow Ico(a,b) \in 𝓝_{\ge a}(a)$$$

Lean4

theorem Ico_mem_nhdsGE (H : a < b) : Ico a b ∈ 𝓝[≥] a :=
  inter_mem_nhdsWithin _ <| Iio_mem_nhds H

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