continuous

Mathlib.Topology.UniformSpace.Equiv

URI: https://scilib.ai/kg/mathlib#UniformEquiv.continuous

English

A uniform equivalence is a continuous map between the underlying spaces.

Русский

Равномерное эквивалентное отображение – непрерывно между пространствами.

LaTeX

$$UniformEquiv.continuous: h → Continuous (h.toEquiv)$$

Lean4

@[continuity]
protected theorem continuous (h : α ≃ᵤ β) : Continuous h :=
  h.uniformContinuous.continuous

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

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

Разделы

Аффилиация

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