of_norm_smul_le — Mathlib

English

If a bilinear bound holds: ∀ r ∈ α, x ∈ β, ‖r • x‖ ≤ ‖r‖ · ‖x‖, then IsBoundedSMul α β holds.

Русский

Если выполнено неравенство: ∀ r ∈ α, x ∈ β, ‖r • x‖ ≤ ‖r‖ · ‖x‖, то IsBoundedSMul α β.

LaTeX

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

Lean4

theorem of_norm_smul_le (h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖) : IsBoundedSMul α β :=
  { dist_smul_pair' := fun a b₁ b₂ => by simpa [smul_sub, dist_eq_norm] using h a (b₁ - b₂)
    dist_pair_smul' := fun a₁ a₂ b => by simpa [sub_smul, dist_eq_norm] using h (a₁ - a₂) b }

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