instClosedIciTopology — Mathlib

English

Left-closed right-infinite intervals [a, ∞) are closed in the lower topology.

Русский

Левые закрытые правые бесконечные интервалы [a, ∞) закрыты в нижней топологии.

LaTeX

$$$\\forall a,\\ IsClosed(\\operatorname{Ici}(a))$ в нижней топологии$$

Lean4

/-- Left-closed right-infinite intervals [a, ∞) are closed in the lower topology. -/
instance : ClosedIciTopology α :=
  ⟨fun a ↦ isOpen_compl_iff.1 <| isOpen_iff_generate_Ici_compl.2 <| GenerateOpen.basic _ ⟨a, rfl⟩⟩

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