English
For any subsets s,t of a group and elements a,b in the group, there exists z such that a•s ∩ b•t is contained in z•((s⁻¹•s) ∩ (t⁻¹•t)).
Русский
Для любых подмножеств S,T группы и элементов a,b существует z such that a•S ∩ b•T ⊆ z•((S⁻¹•S) ∩ (T⁻¹•T)).
LaTeX
$$$\\exists z\\, z \\in \\alpha \\text{ s.t. } a \\cdot S \\cap b \\cdot T \\subseteq z \\cdot\\bigl((S^{-1} \\cdot S) \\cap (T^{-1} \\cdot T)\\bigr)$$$
Lean4
/-- Any intersection of translates of two sets `s` and `t` can be covered by a single translate of
`(s⁻¹ * s) ∩ (t⁻¹ * t)`.
This is useful to show that the intersection of approximate subgroups is an approximate subgroup. -/
@[to_additive /-- Any intersection of translates of two sets `s` and `t` can be covered by a single translate of
`(-s + s) ∩ (-t + t)`.
This is useful to show that the intersection of approximate subgroups is an approximate subgroup.
-/
]
theorem exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul (s t : Set α) (a b : α) :
∃ z : α, a • s ∩ b • t ⊆ z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) :=
by
obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty
· exact ⟨1, by simp [hAB]⟩
refine ⟨z, ?_⟩
calc
a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by gcongr <;> apply smul_set_subset_mul <;> simpa
_ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]
