theorem
IsApproximateSubgroup.prod
{G : Type u_1}
[Group G]
{A : Set G}
{K L : ℝ}
{H : Type u_2}
[Group H]
{B : Set H}
(hA : IsApproximateSubgroup K A)
(hB : IsApproximateSubgroup L B)
:
IsApproximateSubgroup (K * L) (A ×ˢ B)
theorem
IsApproximateAddSubgroup.sum
{G : Type u_1}
[AddGroup G]
{A : Set G}
{K L : ℝ}
{H : Type u_2}
[AddGroup H]
{B : Set H}
(hA : IsApproximateAddSubgroup K A)
(hB : IsApproximateAddSubgroup L B)
:
IsApproximateAddSubgroup (K * L) (A ×ˢ B)
theorem
IsApproximateSubgroup.pi
{ι : Type u_2}
{G : ι → Type u_3}
{s : Finset ι}
[(i : ι) → Group (G i)]
{A : (i : ι) → Set (G i)}
{K : ι → ℝ}
(hA : ∀ i ∈ s, IsApproximateSubgroup (K i) (A i))
:
IsApproximateSubgroup (∏ i ∈ s, K i) ((↑s).pi A)
theorem
IsApproximateAddSubgroup.pi
{ι : Type u_2}
{G : ι → Type u_3}
{s : Finset ι}
[(i : ι) → AddGroup (G i)]
{A : (i : ι) → Set (G i)}
{K : ι → ℝ}
(hA : ∀ i ∈ s, IsApproximateAddSubgroup (K i) (A i))
:
IsApproximateAddSubgroup (∏ i ∈ s, K i) ((↑s).pi A)