Icc_mem_nhdsLE_of_mem — Mathlib

English

Let α be a topological linear order with ClosedIicTopology. If b ∈ Ioc(a,c), then Icc(a,c) is a neighborhood of b within the lower-closed ray {x ≤ b}, i.e., Icc(a,c) ∈ 𝓝[≤] b.

Русский

Пусть α — топологический линейный порядок с ClosedIicTopology. Если b ∈ Ioc(a,c), тогда Icc(a,c) является окрестностью b внутри множества {x ≤ b}, то есть Icc(a,c) ∈ 𝓝[≤] b.

LaTeX

$$$ b \in Ioc(a,c) \implies Icc(a,c) \in 𝓝[≤] b $$$

Lean4

theorem Icc_mem_nhdsLE_of_mem (H : b ∈ Ioc a c) : Icc a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioc_mem_nhdsLE_of_mem H) Ioc_subset_Icc_self

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