English
Under a multiplicative map f, filter A and B by the condition f a = aH and f b = bH, and preserve UniqueMul through this filtered setup.
Русский
При отображении f сохранение UniqueMul через фильтрацию элементов по совпадению с изображениями.
LaTeX
$$UniqueMul (Finset.image (MulHom.funLike.coe f) A) (Finset.image (MulHom.funLike.coe f) B) (MulHom.funLike.coe f a0) (MulHom.funLike.coe f b0) → UniqueMul A B a0 b0$$
Lean4
@[to_additive]
theorem of_image_filter [DecidableEq H] (f : G →ₙ* H) {A B : Finset G} {aG bG : G} {aH bH : H} (hae : f aG = aH)
(hbe : f bG = bH) (huH : UniqueMul (A.image f) (B.image f) aH bH)
(huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG) : UniqueMul A B aG bG := fun a b ha hb he ↦
by
specialize huH (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)
rw [← map_mul, he, map_mul, hae, hbe] at huH
refine huG ?_ ?_ he <;> rw [mem_filter]
exacts [⟨ha, (huH rfl).1⟩, ⟨hb, (huH rfl).2⟩]
