aestabilizer_of_aeconst — Mathlib

English

If s is almost everywhere constant, its ae-stabilizer is the entire group.

Русский

Если s почти везде константа, ae-стабилизатор — вся группа.

LaTeX

$$$(\text{EventuallyConst } s(\mathrm{ae}\,\mu)) \Rightarrow \mathrm{aestabilizer}(G,\mu,s) = \top$$$

Lean4

theorem aestabilizer_of_aeconst (hs : EventuallyConst s (ae μ)) : aestabilizer G μ s = ⊤ :=
  by
  refine top_unique fun g _ ↦ ?_
  cases eventuallyConst_set'.mp hs with
  | inl h => simp [aestabilizer_congr h]
  | inr h => simp [aestabilizer_congr h]

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