const_smul — Mathlib

English

Inseparability is preserved under constant smul: if x ⤳ y is inseparable, then c • x ⤳ c • y for any c ∈ M.

Русский

Неразделимость сохраняется под константным умножением: если x неразделим с y, то c • x неразделим с c • y для любого c.

LaTeX

$$$ x \\;\\mathrel{\\mathrm{Insep}}\\; y \\Rightarrow c \\cdot x \\;\\mathrel{\\mathrm{Insep}}\\; c \\cdot y $$$

Lean4

@[to_additive]
theorem const_smul {x y : α} (h : Inseparable x y) (c : M) : Inseparable (c • x) (c • y) :=
  h.map (continuous_const_smul c)

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