English
If f is nonnegative, multiplicatively bounded, subadditive, preserves zero and negation, and has trivial kernel, then normFromBounded f is a RingNorm on R.
Русский
Если f неотрицательная, ограниченная по умножению, удовлетворяет субаддитивности, сохраняет ноль и отрицание и имеет тривиальное ядро, то normFromBounded f образует RingNorm на R.
LaTeX
$$$f_0=f(0)=0 \land f_\text{nonneg} \ge 0 \land (f(xy) ≤ c f(x) f(y)) \land (f(a+b) ≤ f(a)+f(b)) \land (f(-x)=f(x)) \land (f^{-1}({0})={0}) \Rightarrow \text{normFromBounded } f \text{ is a RingNorm on } R$$$
Lean4
/-- `seminormFromBounded' f` as a `RingNorm` on `R`, provided that `f` is nonnegative,
multiplicatively bounded and subadditive, that it preserves `0` and negation, and that `f` has
trivial kernel. -/
def normFromBounded (f_zero : f 0 = 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y)
(f_add : ∀ a b, f (a + b) ≤ f a + f b) (f_neg : ∀ x : R, f (-x) = f x) (f_ker : f ⁻¹' {0} = {0}) : RingNorm R :=
{ seminormFromBounded f_zero f_nonneg f_mul f_add f_neg with
eq_zero_of_map_eq_zero' := (seminormFromBounded_is_norm_iff f_zero f_nonneg f_mul f_add f_neg).mpr f_ker }
