smul — Mathlib

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

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