iUnion_inv_smul — Mathlib

English

The union over all g of the inverse-smul equals the union over all g of the smul: ⋃ g g⁻¹ • s = ⋃ g g • s.

Русский

Объединение по всем g от обратного действия эквивалентно объединению по прямому действию.

LaTeX

$$$\bigcup_{g\in\alpha} g^{-1}\cdot s = \bigcup_{g\in\alpha} g\cdot s.$$$

Lean4

@[to_additive (attr := simp)]
theorem iUnion_inv_smul : ⋃ g : α, g⁻¹ • s = ⋃ g : α, g • s :=
  (Function.Surjective.iSup_congr _ inv_surjective) fun _ ↦ rfl

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