Theorems · Theorem · Lie groups

compact_open_separated_mul_left

∀ {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, V * K ⊆ U

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

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMulOneClassContinuousMul