Theorems · Theorem · Lie groups

exists_closed_nhds_zero_neg_eq_add_subset

∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {U : Set G},
  U ∈ nhds 0 → ∃ V ∈ nhds 0, IsClosed V ∧ -V = V ∧ V + V ⊆ U

Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V + V ⊆ U.

Defined in

Mathlib.Topology.Algebra.Group.Pointwise

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupIsTopologicalAddGroup