image_coe_inj — Mathlib

English

Two images under quotient construction are equal iff the corresponding subsets are equal modulo N.

Русский

Два образа под конструкцией фактор-группы равны тогда и только тогда, когда соответствующие подмножества равны modulo N.

LaTeX

$$$((\\uparrow) : G \\to Q)'' s = ((\\uparrow) : G \\to Q)'' t \\;\\Leftrightarrow\\; N s = N t$$$

Lean4

@[to_additive]
theorem image_coe_inj {s t : Set G} : ((↑) : G → Q ) '' s = ((↑) : G → Q ) '' t ↔ ↑N * s = N * t :=
  by
  simp_rw [← preimage_image_coe]
  exact QuotientGroup.mk_surjective.preimage_injective.eq_iff.symm

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