pair_eq_mk — Mathlib

English

The pair operation on AEEqFun is representation-equivalent to constructing a mk from the pair of the underlying functions.

Русский

Операция пары на AEEqFun эквивалентна конструированию mk из пары базовых функций.

LaTeX

$$$f.pair g = mk(\lambda x, (f(x), g(x)))\ (f.aestronglyMeasurable.prodMk g.aestronglyMeasurable)$$$

Lean4

theorem pair_eq_mk (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
    f.pair g = mk (fun x => (f x, g x)) (f.aestronglyMeasurable.prodMk g.aestronglyMeasurable) := by
  simp only [← pair_mk_mk, mk_coeFn, f.aestronglyMeasurable, g.aestronglyMeasurable]

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