English
Let 𝕜, 𝕜′ be normed fields and E a normed space over both, with a bilinear action of 𝕜 and 𝕜′ on E. Then the action is continuous when restricted to the closed ball of radius 1 in 𝕜, the closed ball of radius 1 in 𝕜′, and the closed ball of radius r in E, giving a well-defined continuous smul.
Русский
Пусть 𝕜 и 𝕜′ — нормированные поля, E — нормированное пространство над ними; имеется совместное скаляровое действие 𝕜 и 𝕜′ на E. Тогда это действие непрерывно ограничено на замкнутые шаровые множества радиусов 1, 1 и r соответственно.
LaTeX
$$$\text{IsScalarTower}(\text{closedBall}(0,1),\ \text{closedBall}(0,1),\ \text{closedBall}(0,r))$$$
Lean4
instance continuousSMul_sphere_closedBall : ContinuousSMul (sphere (0 : 𝕜) 1) (closedBall (0 : E) r) :=
⟨(continuous_subtype_val.fst'.smul continuous_subtype_val.snd').subtype_mk _⟩
