seminormFromBounded_nonneg — Mathlib

English

The seminorm seminormFromBounded' f is nonnegative.

Русский

Семинорм seminormFromBounded' f неотрицателен.

LaTeX

$$$0 \le \operatorname{seminormFromBounded}' f$$$

Lean4

/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
  `seminormFromBounded' f` is nonnegative. -/
theorem seminormFromBounded_nonneg (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
    0 ≤ seminormFromBounded' f := fun x ↦
  le_csSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) ⟨1, rfl⟩ (div_nonneg (f_nonneg _) (f_nonneg _))

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