English
If f is a map with suitable structure, then IsApproximateSubgroup K (f''A) holds whenever IsApproximateSubgroup K A holds.
Русский
Если f - подходящее отображение, то из IsApproximateSubgroup K A следует IsApproximateSubgroup K (f''A).
LaTeX
$$$\\IsApproximateSubgroup K (f '' A)$$$
Lean4
@[to_additive]
theorem image {F H : Type*} [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F) (hA : IsApproximateSubgroup K A) :
IsApproximateSubgroup K (f '' A) where
one_mem := ⟨1, hA.one_mem, map_one _⟩
inv_eq_self := by simp [← Set.image_inv, hA.inv_eq_self]
sq_covBySMul := by
classical
obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul
refine ⟨F.image f, ?_, ?_⟩
·
calc
(#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
_ ≤ K := hF
· simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
gcongr
