English
If a and b are inseparable and x and y are inseparable, then a•x and b•y are inseparable.
Русский
Если a и b неразделимы, а x и y также неразделимы, то a•x и b•y also неразделимы.
LaTeX
$$$Inseparable\ a\ b \Rightarrow Inseparable\ x\ y \Rightarrow Inseparable\ (a \cdot x)\ (b \cdot y)$$$
Lean4
@[to_additive]
protected theorem smul {a b : M} {x y : X} (h₁ : Inseparable a b) (h₂ : Inseparable x y) :
Inseparable (a • x) (b • y) :=
(h₁.prod h₂).map continuous_smul