Theorems · Theorem · Lie groups

exists_open_nhds_zero_add_subset

∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [ContinuousAdd M] {U : Set M},
  U ∈ nhds 0 → ∃ V, IsOpen V ∧ 0 ∈ V ∧ V + V ⊆ U

Given an open neighborhood U of 0 there is an open neighborhood V of 0 such that V + V ⊆ U.

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddZeroClassContinuousAdd