measurableEmbedding_const_smul₀

English

If c ≠ 0 in a group with zero, then x ↦ c • x yields a measurable embedding of α.

Русский

Если c ≠ 0 в группе с нулём, то отображение x ↦ c • x даёт измеримое вложение α.

LaTeX

$$$$ c \\neq 0 \\Rightarrow \\text{MeasurableEmbedding}(c \\cdot -: \\alpha \\to \\alpha). $$$$

Lean4

theorem _root_.measurableEmbedding_const_smul₀ {c : G₀} (hc : c ≠ 0) : MeasurableEmbedding (c • · : α → α) :=
  (smul₀ c hc).measurableEmbedding

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