smul — Mathlib

English

If x almost-maps s to itself, then x^{-1} almost-maps s to itself.

Русский

Если x почти отображает s в себя, то x^{-1} тоже отображает s в себя почти наверняка.

LaTeX

$$$\forall hs: (x\cdot s =^{\mu} s),\ (x^{-1}\cdot s =^{\mu} s)$$$

Lean4

@[to_additive]
instance smul [SMulInvariantMeasure M α μ] (c : ℝ≥0∞) : SMulInvariantMeasure M α (c • μ) :=
  ⟨fun a _s hs => show c • _ = c • _ from congr_arg (c • ·) (measure_preimage_smul a hs)⟩

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