Theorems · Theorem · Lie groups

compact_covered_by_mul_left_translates

∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {K V : Set G},
  IsCompact K → (interior V).Nonempty → ∃ t, K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V

A compact set is covered by finitely many left multiplicative translates of a set with non-empty interior.

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroup