English
For families α_i → β_i indexed by ι, if each action is bounded, then the product action on ∀ i, α_i → ∀ i, β_i is bounded.
Русский
Для семейств α_i → β_i, если каждое действие ограничено, то произведение действует ограниченно на ∀ i, α_i → ∀ i, β_i.
LaTeX
$$$IsBoundedSMul(\\forall i, α_i) (\\forall i, β_i)$$$
Lean4
instance instIsBoundedSMul' {α β : ι → Type*} [∀ i, PseudoMetricSpace (α i)] [∀ i, PseudoMetricSpace (β i)]
[∀ i, Zero (α i)] [∀ i, Zero (β i)] [∀ i, SMul (α i) (β i)] [∀ i, IsBoundedSMul (α i) (β i)] :
IsBoundedSMul (∀ i, α i) (∀ i, β i)
where
dist_smul_pair' x y₁
y₂ :=
(dist_pi_le_iff <| by positivity).2 fun _ ↦
(dist_smul_pair _ _ _).trans <| mul_le_mul (dist_le_pi_dist _ 0 _) (dist_le_pi_dist _ _ _) dist_nonneg dist_nonneg
dist_pair_smul' x₁ x₂
y :=
(dist_pi_le_iff <| by positivity).2 fun _ ↦
(dist_pair_smul _ _ _).trans <| mul_le_mul (dist_le_pi_dist _ _ _) (dist_le_pi_dist _ 0 _) dist_nonneg dist_nonneg
