extension₂_coe_coe — Mathlib

English

For uncurry f with uniform continuity, the 2-ary extension on (ι a, ι b) equals f a b.

Русский

Для раскрученного f с равномерной непрерывностью продолжение на паре (ι a, ι b) даёт f a b.

LaTeX

$$$ (hf: UniformContinuous \ (uncurry\ f)) \to (a:\alpha) (b:\beta), \ pkg.extend₂ pkg' f (ι a) (ι' b) = f a b $$$

Lean4

theorem extension₂_coe_coe (hf : UniformContinuous <| uncurry f) (a : α) (b : β) :
    pkg.extend₂ pkg' f (ι a) (ι' b) = f a b :=
  show (pkg.prod pkg').extend (uncurry f) ((pkg.prod pkg').coe (a, b)) = uncurry f (a, b) from
    (pkg.prod pkg').extend_coe hf _

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