continuous_uliftUp

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#continuous_uliftUp

← MathLib Explorer

English

The map ULift.up: X → ULift X is continuous.

Русский

Отображение ULift.up: X → ULift X непрерывно.

LaTeX

$$$\mathrm{Continuous}(\mathrm{ULift.up}).$$$

Lean4

@[continuity, fun_prop]
theorem continuous_uliftUp [TopologicalSpace X] : Continuous (ULift.up : X → ULift.{v, u} X) :=
  continuous_induced_rng.2 continuous_id

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru