Theorems · Theorem · Lie groups

exists_closed_nhds_one_inv_eq_mul_subset

∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {U : Set G},
  U ∈ nhds 1 → ∃ V ∈ nhds 1, 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

TopologicalSpaceGroupIsTopologicalGroup