Theorems · Theorem · Lie groups

compact_open_separated_add_right

∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddZeroClass G] [ContinuousAdd G] {K U : Set G},
  IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 0, K + V ⊆ U

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

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddZeroClassContinuousAdd