preimage_image_coe — Mathlib

English

Characterizes the preimage of the image of a set under the quotient map in terms of the normal subgroup N and the set.

Русский

Характеризуется предобраз образа множества под фактор-группой через нормальную подгруппу N и множество.

LaTeX

$$$\\mathrm{preimage} \\; (\\mathrm{mk}) \\left( \\mathrm{image} \\; \\mathrm{mk} \\; s \\right) = N \\cdot s.$$$

Lean4

@[to_additive]
theorem preimage_image_coe (s : Set G) : ((↑) : G → Q ) ⁻¹' ((↑) '' s) = N * s :=
  by
  ext a
  constructor
  · rintro ⟨b, hb, h⟩
    refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
    simp only [h, QuotientGroup.mk_div, div_self']
  · rintro ⟨a, ha, b, hb, rfl⟩
    refine ⟨b, hb, ?_⟩
    simpa only [QuotientGroup.mk_mul, right_eq_mul, QuotientGroup.eq_one_iff]

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