eq_of_empty

Mathlib.Topology.ContinuousMap.Bounded.Basic

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.eq_of_empty

English

If α is empty, any two bounded continuous functions are equal.

Русский

Если область определения пустая, любые две ограниченно непрерывные функции равны.

LaTeX

$$$[\text{IsEmpty } \alpha] \; (f,g : \alpha \to^b \beta) \Rightarrow f = g$$$

Lean4

theorem eq_of_empty [h : IsEmpty α] (f g : α →ᵇ β) : f = g :=
  ext <| h.elim

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

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

Разделы

Аффилиация

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