Theorems · Theorem · Lie groups

compact_open_separated_mul_right

∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : MulOneClass G] [ContinuousMul G] {K U : Set G},
  IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 1, K * V ⊆ U

Given a compact set K inside an open set U, there is an open neighborhood V of 1 such that K * V ⊆ U.

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMulOneClassContinuousMul