Iic_mem_nhdsSet_Ico — Mathlib

English

In an order-closed topology, for any a,b,c with b ≤ c, the left-closed interval up to c, Iic c, is a neighborhood (in the nhds-set sense) of the half-open interval Ico a b.

Русский

В пространстве с порядком и замыканием по порядку, для любых a,b,c с b ≤ c, левая граница Iic c является окрестностью множества Ico a b в смысле nhdsSet.

LaTeX

$$$[TopologicalSpace\, \alpha]\ [OrderClosedTopology\, \alpha]\forall a,b,c:\alpha\, (h: b\le c) \Rightarrow Iic\ c \in 𝓝ˢ(Ico\ a\ b).$$$

Lean4

theorem Iic_mem_nhdsSet_Ico (h : b ≤ c) : Iic c ∈ 𝓝ˢ (Ico a b) :=
  mem_of_superset (Iio_mem_nhdsSet_Ico h) Iio_subset_Iic_self

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