smul_ae_eq_self_of_mem_zpowers — Mathlib

English

If x almost-sends s to itself and y lies in the z-powers of x, then y also almost-sends s to itself.

Русский

Если x почти переводит s в себя, и y принадлежит z-пу.pow(x), то и y поддерживает это почти повсюду.

LaTeX

$$$(x\cdot s =^{\mu} s) \land (y \in \mathrm{zpowers}(x)) \Rightarrow (y\cdot s =^{\mu} s)$$$

Lean4

@[to_additive]
theorem smul_ae_eq_self_of_mem_zpowers (hs : (x • s : Set α) =ᵐ[μ] s) (hy : y ∈ Subgroup.zpowers x) :
    (y • s : Set α) =ᵐ[μ] s :=
  by
  rw [← MulAction.mem_aestabilizer, ← Subgroup.zpowers_le] at hs
  exact hs hy

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