isBoundedSMul — Mathlib

English

Multiplication in β is continuous as a map β × β → β.

Русский

Умножение в β является непрерывной операцией на β × β → β.

LaTeX

$$$\\text{ContinuousMul }\\beta$$$

Lean4

instance isBoundedSMul : IsBoundedSMul ℝ≥0 ℝ≥0
    where
  dist_smul_pair' x y₁ y₂ := by convert dist_smul_pair (x : ℝ) (y₁ : ℝ) y₂ using 1
  dist_pair_smul' x₁ x₂ y := by convert dist_pair_smul (x₁ : ℝ) x₂ (y : ℝ) using 1

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