English
Given two compact sets K and L in a noncompact topological group, there exists a translate g · L disjoint from K.
Русский
Для двух компактных множеств K и L в некомпактной топологической группе существует перенос g · L, который не пересекается с K.
LaTeX
$$$\exists g \in G,\; K \cap (g \cdot L) = \emptyset.$$$
Lean4
/-- Given two compact sets in a noncompact topological group, there is a translate of the second
one that is disjoint from the first one. -/
@[to_additive /-- Given two compact sets in a noncompact additive topological group, there is a
translate of the second one that is disjoint from the first one. -/
]
theorem exists_disjoint_smul_of_isCompact [NoncompactSpace G] {K L : Set G} (hK : IsCompact K) (hL : IsCompact L) :
∃ g : G, Disjoint K (g • L) :=
by
have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ
obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹ := by
contrapose! A
exact eq_univ_iff_forall.2 A
refine ⟨g, ?_⟩
refine disjoint_left.2 fun a ha h'a => hg ?_
rcases h'a with ⟨b, bL, rfl⟩
refine ⟨g * b, ha, b⁻¹, by simpa only [Set.mem_inv, inv_inv] using bL, ?_⟩
simp only [mul_inv_cancel_right]
