seminormFromBounded_one_le — Mathlib

English

seminormFromBounded' f 1 ≤ 1.

Русский

seminormFromBounded' f 1 ≤ 1.

LaTeX

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

Lean4

/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
  `seminormFromBounded' f 1 ≤ 1`. -/
theorem seminormFromBounded_one_le (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
    seminormFromBounded' f 1 ≤ 1 := by
  by_cases f_ne_zero : f ≠ 0
  · exact le_of_eq (seminormFromBounded_one f_ne_zero f_nonneg f_mul)
  · simp_rw [seminormFromBounded', one_mul]
    refine ciSup_le (fun _ ↦ ?_)
    push_neg at f_ne_zero
    simp only [f_ne_zero, Pi.zero_apply, div_zero, zero_le_one]

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