smul_boundedBy — Mathlib

English

For c ≠ ∞, c • boundedBy m = boundedBy (c • m).

Русский

При c ≠ ∞ имеем c • boundedBy m = boundedBy (c • m).

LaTeX

$$$\\forall c \\; (c \\neq \\infty)\\; :\\; c \\cdot \\mathrm{boundedBy}(m) = \\mathrm{boundedBy}(c \\cdot m)$$$

Lean4

theorem smul_boundedBy {c : ℝ≥0∞} (hc : c ≠ ∞) : c • boundedBy m = boundedBy (c • m) :=
  by
  simp only [boundedBy, smul_ofFunction hc]
  congr 1 with s : 1
  rcases s.eq_empty_or_nonempty with (rfl | hs) <;> simp [*]

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