comp₂_eq_pair — Mathlib

English

The equality of two pairs of AEEqFun is equivalent to the equality of their mk-paired underlying functions.

Русский

Равенство двух пар функций эквивалентно равенству соответствующих функций-пар в mk.

LaTeX

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

Lean4

theorem comp₂_eq_pair (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
    comp₂ g hg f₁ f₂ = comp _ hg (f₁.pair f₂) :=
  rfl

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