preimage_image_mk_eq_mul — Mathlib

English

The preimage under the quotient map of the image of a family is the product of the family with the subgroup, i.e., the coset structure covers the ambient subgroup by left multiplication.

Русский

Предобраз образа под квотирующей картой равен произведению семейства на подгруппу, т.е. вся группа покрывается левой нормой.

LaTeX

$$$\text{preimage}(\text{QuotientGroup.mk}, \text{image}(\text{QuotientGroup.mk} \, s)) = s \cdot N$$$

Lean4

@[to_additive]
theorem preimage_image_mk_eq_mul (N : Subgroup α) (s : Set α) : mk ⁻¹' ((mk : α → α ⧸ N) '' s) = s * N :=
  by
  rw [preimage_image_mk_eq_iUnion_image, iUnion_subtype, ← image2_mul, ← iUnion_image_right]
  simp only [SetLike.mem_coe]

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