continuous

Mathlib.Geometry.Manifold.IsManifold.Basic

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

English

The coordinate map I.toFun' is continuous; the model induces a continuous coordinate representation.

Русский

Координатное отображение I.toFun' непрерывно; модель порождает непрерывное координатное представление.

LaTeX

$$$ \\text{Continuous}(I.toFun') $$$

Lean4

@[fun_prop]
protected theorem continuous : Continuous I :=
  I.continuous_toFun

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

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

Разделы

Аффилиация

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