Theorems · Theorem · commutative algebra

seminormFromBounded_is_norm_iff

∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ} (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 : R), f (a + b) ≤ f a + f b)
  (f_neg : ∀ (x : R), f (-x) = f x),
  (∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0}

If f : R → ℝ is a nonnegative, multiplicatively bounded, subadditive function that preserves zero and negation, then seminormFromBounded' f is a norm if and only if f⁻¹' {0} = {0}.

Defined in

Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Cited by

0 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing