measurableEmbedding_const_smul — Mathlib

English

For each c ∈ G, the map x ↦ c • x is a measurable embedding of α.

Русский

Для каждого фиксированного c ∈ G отображение x ↦ c • x является измеримым вложением α.

LaTeX

$$$$ \\forall c \\in G,\\; \\text{MeasurableEmbedding}(c \\cdot -: \\alpha \\to \\alpha). $$$$

Lean4

@[to_additive]
theorem _root_.measurableEmbedding_const_smul (c : G) : MeasurableEmbedding (c • · : α → α) :=
  (smul c).measurableEmbedding

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