pair_apply

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.pair_apply

English

The value of pair f g at a is (f a, g a).

Русский

Значение pair f g в точке a равно (f(a), g(a)).

LaTeX

$$$$ pair\\, f\\, g\\, a = (f\\, a,\; g\\, a). $$$$

Lean4

@[simp]
theorem pair_apply (f : α →ₛ β) (g : α →ₛ γ) (a) : pair f g a = (f a, g a) :=
  rfl

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

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

Разделы

Аффилиация

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