of_enorm_smul_le — Mathlib

English

If one has a bound for ENorm smul: ∀ r x, ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ, then IsBoundedSMul α β holds.

Русский

Если есть ограничение для ENorm-умножения: ∀ r x, ‖r • x‖ₑ ≤ ‖r‖ₑ · ‖x‖ₑ, то IsBoundedSMul α β.

LaTeX

$$$IsBoundedSMul\\;\\alpha\\;\\beta$$$

Lean4

theorem of_enorm_smul_le (h : ∀ (r : α) (x : β), ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ) : IsBoundedSMul α β :=
  .of_norm_smul_le (by simpa [enorm_eq_nnnorm, ← ENNReal.coe_mul, ENNReal.coe_le_coe] using h)

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