continuous_const

Mathlib.Topology.Continuous

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

English

A constant function f: X → Y is continuous on X.

Русский

Постоянная функция f: X → Y непрерывна на X.

LaTeX

$$$\\mathrm{Continuous}(f)$ if $f$ is constant$$

Lean4

@[continuity, fun_prop]
theorem continuous_const : Continuous fun _ : X => y :=
  continuous_iff_continuousAt.mpr fun _ => continuousAt_const

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

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

Разделы

Аффилиация

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