pi_norm_le_iff_of_nonempty' — Mathlib

English

Assume ι is nonempty. For f : ι → G_i and r ∈ ℝ, we have ∥f∥ ≤ r if and only if ∀ b ∈ ι, ∥f(b)∥ ≤ r.

Русский

Пусть множество индексов ι непустое. Для f : ι → G_i и r ∈ ℝ верно: ∥f∥ ≤ r тогда и только если для каждого b ∈ ι выполняется ∥f(b)∥ ≤ r.

LaTeX

$$$\|f\| \le r \iff \forall b, \|f(b)\| \le r$$$

Lean4

@[to_additive pi_norm_le_iff_of_nonempty]
theorem pi_norm_le_iff_of_nonempty' [Nonempty ι] : ‖f‖ ≤ r ↔ ∀ b, ‖f b‖ ≤ r :=
  by
  by_cases hr : 0 ≤ r
  · exact pi_norm_le_iff_of_nonneg' hr
  ·
    exact
      iff_of_false (fun h => hr <| (norm_nonneg' _).trans h) fun h =>
        hr <| (norm_nonneg' _).trans <| h <| Classical.arbitrary _

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