continuousSMul_sphere_sphere — Mathlib

English

Consider the action of the unit sphere on the radius-r sphere; the action is well-defined and respects the sphere structure.

Русский

Рассмотрим действие единичной сферы на сферу радиуса r; действие определено и согласуется со структурой сферы.

LaTeX

$$$\text{ContinuousSMul}(\text{sphere}(0,1),\text{sphere}(0,r))$$$

Lean4

instance continuousSMul_sphere_sphere : ContinuousSMul (sphere (0 : 𝕜) 1) (sphere (0 : E) r) :=
  ⟨(continuous_subtype_val.fst'.smul continuous_subtype_val.snd').subtype_mk _⟩

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