Ioc_mem_nhdsLE_of_mem — Mathlib

English

Let α be a topological linear order with ClosedIicTopology. If b lies in the interval Ioc(a,c), then Ioc(a,c) is a neighborhood of b within the lower-closed ray {x ≤ b}. In other words, Ioc(a,c) ∈ 𝓝[≤] b whenever b ∈ Ioc(a,c).

Русский

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

LaTeX

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

Lean4

theorem Ioc_mem_nhdsLE_of_mem (H : b ∈ Ioc a c) : Ioc a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioc_mem_nhdsLE H.1) <| Ioc_subset_Ioc_right H.2

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