coeFn_pair

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.coeFn_pair

English

Almost everywhere, the function produced by pairing equals the pair of the function values.

Русский

Почти везде функция, полученная парой, равна паре значений функций.

LaTeX

$$$f.pair g =^{\mu}_{ae} (x \mapsto (f(x), g(x)))$$$

Lean4

theorem coeFn_pair (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : f.pair g =ᵐ[μ] fun x => (f x, g x) :=
  by
  rw [pair_eq_mk]
  apply coeFn_mk

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

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

Разделы

Аффилиация

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