forall_coe_one_iff_one

Mathlib.Topology.ContinuousMap.Bounded.Basic

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

English

f equals the constant-1 function if and only if every evaluation f(x) equals 1.

Русский

f равно константе 1 тогда и только тогда, когда для всех x выполнено f(x)=1.

LaTeX

$$$(\\forall x:\\alpha, f(x) = 1) \\; \\Leftrightarrow \\; f = 1$$$

Lean4

@[to_additive]
theorem forall_coe_one_iff_one (f : α →ᵇ β) : (∀ x, f x = 1) ↔ f = 1 :=
  (@DFunLike.ext_iff _ _ _ _ f 1).symm

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

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

Разделы

Аффилиация

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