seminormFromBounded' — Mathlib

English

The function seminormFromBounded' f defines a ring seminorm on R, provided f(0)=0, f is nonnegative, f is multiplicatively bounded, f is subadditive, and f(-x)=f(x).

Русский

Функция seminormFromBounded' f задаёт кольцевой семинорм на R при условии, что f(0)=0, f неотрицательно, ограничено умножением, субаддитивна и f(-x)=f(x).

LaTeX

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

Lean4

/-- The real-valued function sending `x ∈ R` to the supremum of  `f(x*y)/f(y)`, where `y` runs over
the elements of `R`. -/
def seminormFromBounded' : R → ℝ := fun x ↦ iSup fun y : R ↦ f (x * y) / f y

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