seminormFromBounded_le — Mathlib

English

For NormedRing, the RingNorm applied to an element x yields its norm.

Русский

Для NormedRing применение RingNorm к элементу x даёт норму этого элемента.

LaTeX

$$$(\text{NormedRing.toRingNorm } R)\, x = \|x\|$$$

Lean4

/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then for every `x : R`,
  `seminormFromBounded' f x` is bounded above by some multiple of `f x`. -/
theorem seminormFromBounded_le (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) :
    seminormFromBounded' f x ≤ c * f x := by
  refine ciSup_le (fun y ↦ ?_)
  rcases (f_nonneg y).eq_or_lt' with hy | hy
  · simpa [hy] using seminormFromBounded_aux f_nonneg f_mul x
  · rw [div_le_iff₀ hy]
    apply f_mul

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