seminormFromBounded — Mathlib

English

seminormFromBounded' f is a RingSeminorm on R.

Русский

seminormFromBounded' f — кольцевая семинормa на R.

LaTeX

$$$\operatorname{seminormFromBounded}' f \text{ is a RingSeminorm on } R$$$

Lean4

/-- `seminormFromBounded'` is a ring seminorm on `R`. -/
def seminormFromBounded (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) : RingSeminorm R
    where
  toFun := seminormFromBounded' f
  map_zero' := seminormFromBounded_zero f_zero
  add_le' := seminormFromBounded_add f_nonneg f_mul f_add
  mul_le' := seminormFromBounded_mul f_nonneg f_mul
  neg' := seminormFromBounded_neg f_neg

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