measurableEmbedding_mulLeft₀ — Mathlib

English

If g ≠ 0 in G₀, then the map x ↦ g x is a measurable embedding of G into itself.

Русский

Если g ≠ 0 в G₀, то отображение x ↦ g x является измеримым вложением G в себя.

LaTeX

$$$g \\neq 0 \\;\\Rightarrow\\; \\text{MeasurableEmbedding}(x \\mapsto g x)$$$

Lean4

theorem _root_.measurableEmbedding_mulLeft₀ {g : G₀} (hg : g ≠ 0) : MeasurableEmbedding (g * ·) :=
  (mulLeft₀ g hg).measurableEmbedding

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