continuousOn_empty

Mathlib.Topology.ContinuousOn

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

English

Any function is continuously defined on the empty set.

Русский

Любая функция непрерывна на пустом множестве.

LaTeX

$$$\\text{ContinuousOn } f \\varnothing$$$

Lean4

@[simp]
theorem continuousOn_empty (f : α → β) : ContinuousOn f ∅ := fun _ => False.elim

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

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

Разделы

Аффилиация

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