English
If f is nonzero, nonnegative, and multiplicatively bounded, then the associated seminorm seminormFromBounded' f is nonzero.
Русский
Если f не ноль, неотрицательная и ограниченная по умножению, то соответствующий сепиномор seminormFromBounded' f не ноль.
LaTeX
$$$\{f\neq 0\} \land (0 \le f) \land (\forall x,y,\ f(xy) \le c f(x) f(y)) \Rightarrow \ seminormFromBounded' f \\neq 0$$$
Lean4
/-- If `f : R → ℝ` is a nonzero, nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f` is nonzero. -/
theorem seminormFromBounded_nonzero (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f)
(f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) : seminormFromBounded' f ≠ 0 :=
by
obtain ⟨x, hx⟩ := Function.ne_iff.mp f_ne_zero
rw [Function.ne_iff]
use x
rw [ne_eq, Pi.zero_apply, seminormFromBounded_eq_zero_iff f_nonneg f_mul x]
exact hx
