English
If α acts by bounded scalar multiplication on each β_i, then α acts boundedly on the product space ∀ i, β_i.
Русский
Если на каждом β_i действует ограниченное скалярное умножение со стороны α, то α действует ограниченно на произведении ∀ i, β_i.
LaTeX
$$$\\left( \\forall i, IsBoundedSMul(\\alpha, \\beta_i) \\right) \\Rightarrow IsBoundedSMul(\\alpha, \\forall i, \\beta_i)$$$
Lean4
instance instIsBoundedSMul {α : Type*} {β : ι → Type*} [PseudoMetricSpace α] [∀ i, PseudoMetricSpace (β i)] [Zero α]
[∀ i, Zero (β i)] [∀ i, SMul α (β i)] [∀ i, IsBoundedSMul α (β i)] : IsBoundedSMul α (∀ i, β i)
where
dist_smul_pair' x y₁
y₂ :=
(dist_pi_le_iff <| by positivity).2 fun _ ↦
(dist_smul_pair _ _ _).trans <| mul_le_mul_of_nonneg_left (dist_le_pi_dist _ _ _) dist_nonneg
dist_pair_smul' x₁ x₂
y :=
(dist_pi_le_iff <| by positivity).2 fun _ ↦
(dist_pair_smul _ _ _).trans <| mul_le_mul_of_nonneg_left (dist_le_pi_dist _ 0 _) dist_nonneg
