prod_continuous_ofLp

Mathlib.Analysis.Normed.Lp.ProdLp

URI: https://scilib.ai/kg/mathlib#WithLp.prod_continuous_ofLp

English

Continuity of the embedding of α × β into WithLp p (α × β): ofLp p (α × β) is continuous.

Русский

Непрерывность вложения $α × β$ в WithLp p (α × β): ofLp p (α × β) непрерывно.

LaTeX

$$$$\\text{Continuous}(\\operatorname{WithLp}.ofLp\\, p\\, (α × β))$$$$

Lean4

@[continuity, fun_prop]
theorem prod_continuous_ofLp : Continuous (@ofLp p (α × β)) :=
  continuous_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru