continuous_inducingFn — Mathlib

English

The inducingFn is continuous as a map from the weak operator topology space to the product space.

Русский

Функция inducingFn непрерывна как отображение из пространства слабой операторной топологии в произведение.

LaTeX

$$$\\text{continuous\\_inducingFn}: \\text{Continuous}(\\text{inducingFn})$$$

Lean4

@[fun_prop]
theorem continuous_inducingFn : Continuous (inducingFn 𝕜 E F) :=
  continuous_induced_dom

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