intCast_apply

Mathlib.Topology.ContinuousMap.Bounded.Basic

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

English

If β has an IntCast, then the integer m acts as a constant function on α, i.e., (m: α →ᵇ β)(x) = m for all x.

Русский

Если у β есть IntCast, целое m действует как константная функция: (m: α →ᵇ β)(x) = m для всех x.

LaTeX

$$$[\text{IntCast }(\alpha \to^{\mathrm{b}} \beta)](m)(x) = m$$$

Lean4

@[simp]
theorem intCast_apply [IntCast β] (m : ℤ) (x : α) : (m : α →ᵇ β) x = m :=
  rfl

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

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

Разделы

Аффилиация

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