continuous₂ — Mathlib

English

Useful to combine two linear maps into a continuous map by uncurry; the map (x,y) ↦ f x y is continuous.

Русский

Удобно использовать каррирование/некуррирование, чтобы получить непрерывное отображение из пары линейных отображений.

LaTeX

$$$Continuous (Function.uncurry (\lambda x y => f x y))$$$

Lean4

/-- Useful to use together with `Continuous.comp₂`. -/
theorem continuous₂ (f : E →L[𝕜] F →L[𝕜] G) : Continuous (Function.uncurry fun x y => f x y) :=
  f.isBoundedBilinearMap.continuous

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