extension₂_coe_coe — Mathlib

English

For hf uniform continuous₂, the two-argument extension on embedded a and b matches f a b.

Русский

Для hf, непрерывной двойной, расширение на встроенных элементах совпадает с f(a,b).

LaTeX

$$$\\mathrm{Completion.extension_2} f\\; (\\mathrm{coe}' a)\\; (\\mathrm{coe}' b) = f a b$$$

Lean4

theorem extension₂_coe_coe (hf : UniformContinuous₂ f) (a : α) (b : β) : Completion.extension₂ f a b = f a b :=
  cPkg.extension₂_coe_coe cPkg hf a b

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