Theorems · Theorem · Lie groups

exists_disjoint_smul_of_isCompact

∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [NoncompactSpace G] {K L : Set G},
  IsCompact K → IsCompact L → ∃ g, Disjoint K (g • L)

Given two compact sets in a noncompact topological group, there is a translate of the second one that is disjoint from the first one.

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceGroupIsTopologicalGroupNoncompactSpace