aestabilizer_congr — Mathlib

English

If s and t are a.e.-equal, their a.e.-stabilizers coincide.

Русский

Если s и t равны почти всюду, их ae-стабилизаторы совпадают.

LaTeX

$$$s =^{\mu} t \Rightarrow \mathrm{aestabilizer}(G,\mu,s) = \mathrm{aestabilizer}(G,\mu,t)$$$

Lean4

@[to_additive]
theorem aestabilizer_congr (h : s =ᵐ[μ] t) : aestabilizer G μ s = aestabilizer G μ t :=
  by
  ext g
  rw [mem_aestabilizer, mem_aestabilizer, h.congr_right, ((smul_set_ae_eq g).2 h).congr_left]

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