continuous_toLower — Mathlib

English

If α is a topological space and has ClosedIciTopology, then the natural map toLower: α → WithLower α is continuous.

Русский

Если α является топологическим пространством и обладает свойством ClosedIciTopology, то естественное отображение toLower: α → WithLower α непрерывно.

LaTeX

$$$[\\text{TopologicalSpace } \\alpha] \\, [\\text{ClosedIciTopology } \\alpha] : \\mathrm{Continuous}(\\operatorname{toLower} : \\alpha \\to \\mathrm{WithLower} \\alpha)$$$

Lean4

theorem continuous_toLower [TopologicalSpace α] [ClosedIciTopology α] : Continuous (toLower : α → WithLower α) :=
  continuous_generateFrom_iff.mpr <| by rintro _ ⟨a, rfl⟩; exact isClosed_Ici.isOpen_compl

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