continuous

Mathlib.Topology.Path

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

English

A path γ is a continuous map from the unit interval to X.

Русский

Путь γ является непрерывной отображением от единичного отрезка к X.

LaTeX

$$$\text{protected theorem continuous }(\gamma) : \text{Continuous}(\gamma)$$$

Lean4

@[continuity]
protected theorem continuous : Continuous γ :=
  γ.continuous_toFun

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

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

Разделы

Аффилиация

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