English
If α acts boundedly on β and on γ, then α acts boundedly on the product β × γ.
Русский
Если α действует ограниченно на β и на γ, то α действует ограниченно на произведение β × γ.
LaTeX
$$$IsBoundedSMul(\\alpha, \\beta) \\land IsBoundedSMul(\\alpha, \\gamma) \\Rightarrow IsBoundedSMul(\\alpha, \\beta \\times \\gamma)$$$
Lean4
instance instIsBoundedSMul {α β γ : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] [Zero α]
[Zero β] [Zero γ] [SMul α β] [SMul α γ] [IsBoundedSMul α β] [IsBoundedSMul α γ] : IsBoundedSMul α (β × γ)
where
dist_smul_pair' _x _y₁
_y₂ :=
max_le ((dist_smul_pair _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_left _ _) dist_nonneg)
((dist_smul_pair _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_right _ _) dist_nonneg)
dist_pair_smul' _x₁ _x₂
_y :=
max_le ((dist_pair_smul _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_left _ _) dist_nonneg)
((dist_pair_smul _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_right _ _) dist_nonneg)
