continuous_toUpper — Mathlib

English

If α is a topological space and ClosedIicTopology α, then Continuous (toUpper : α → WithUpper α).

Русский

Если α является топологическим пространством и имеет ClosedIicTopology α, то отображение toUpper: α → WithUpper α непрерывно.

LaTeX

$$$\\forall \\alpha,\\ [\\mathrm{TopologicalSpace}\\ \\alpha]\\ [\\mathrm{ClosedIicTopology}\\ \\alpha] : \\mathrm{Continuous}(\\operatorname{toUpper} : \\alpha \\to \\mathrm{WithUpper} \\alpha)$$$

Lean4

theorem continuous_toUpper [TopologicalSpace α] [ClosedIicTopology α] : Continuous (toUpper : α → WithUpper α) :=
  continuous_generateFrom_iff.mpr <| by rintro _ ⟨a, rfl⟩; exact isClosed_Iic.isOpen_compl

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