sound — Mathlib

English

In a quotient construction, the action by elements of the base subgroup on the preimage of a set in the quotient leaves the preimage invariant.

Русский

В конструкции фактора действие элементов базовой подгруппы на прообраз множества в фактор-группе сохраняет прообраз неизменным.

LaTeX

$$$g \\cdot (mk'\\ N)^{-1}' U = (mk'\\ N)^{-1}' U$ for all U and g in N$$

Lean4

@[to_additive]
theorem sound (U : Set (G ⧸ N)) (g : N.op) : g • (mk' N) ⁻¹' U = (mk' N) ⁻¹' U :=
  by
  ext x
  simp only [Set.mem_preimage, Set.mem_smul_set_iff_inv_smul_mem]
  congr! 1
  exact
    Quotient.sound
      ⟨g⁻¹, rfl⟩
        -- for commutative groups we don't need normality assumption

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