le_of_opNNNorm_le

Mathlib.Analysis.NormedSpace.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.le_of_opNNNorm_le

English

Similarly, the NNReal norm of pi f equals the NNReal norm of f.

Русский

Аналогично, nnnorm(pi f) = nnnorm(f).

LaTeX

$$$$\|\pi f\|_{+} = \|f\|_{+}.$$$$

Lean4

theorem le_of_opNNNorm_le {C : ℝ≥0} (h : ‖f‖₊ ≤ C) (m : ι → E) : ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊ :=
  f.1.le_of_opNNNorm_le h m

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

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

Разделы

Аффилиация

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