continuous_symm

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.continuous_symm

English

Let I be the unit interval [0,1], and σ the map t ↦ 1 − t. Then σ is continuous.

Русский

Пусть I — единичный отрезок [0,1], а σ — отображение t ↦ 1 − t. Тогда σ непрерывно.

LaTeX

$$$\sigma: I \to I,\ \sigma(t)=1-t,\ \sigma \in C(I,I)$$$

Lean4

@[continuity, fun_prop]
theorem continuous_symm : Continuous σ :=
  Continuous.subtype_mk (by fun_prop) _

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

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

Разделы

Аффилиация

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