Theorems · Theorem · commutative algebra

seminormFromBounded_mul

∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f →
    (∀ (x y : R), f (x * y) ≤ c * f x * f y) →
      ∀ (x y : R), seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f is submultiplicative.

Defined in: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Cited by: 0 results in Mathlib
Foundations: Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
CommRingstatement and proof · cited by 17,173
mul_commproof · cited by 2,262
le_reflproof · cited by 2,061
mul_assocproof · cited by 1,667
mul_nonnegproof · cited by 397
zero_divproof · cited by 222
lt_of_le_of_ne'proof · cited by 149
div_nonnegproof · cited by 103
div_le_iff₀proof · cited by 97
ciSup_leproof · cited by 56
div_mul_eq_mul_divproof · cited by 51

Cited by1

Results whose statement or proof uses this declaration.

seminormFromBoundedproof · cited by 2