Theorems · Theorem · Lie groups

Set.univ_smul_nhds_zero

∀ {G₀ : Type u_5} {X : Type u_6} [inst : GroupWithZero G₀] [inst_1 : Zero X] [inst_2 : MulActionWithZero G₀ X]
  [inst_3 : TopologicalSpace G₀] [(nhdsWithin 0 {0}ᶜ).NeBot] [inst_5 : TopologicalSpace X] [ContinuousSMul G₀ X]
  {s : Set X}, s ∈ nhds 0 → Set.univ • s = Set.univ

Defined in

Mathlib.Topology.Algebra.MulAction

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupWithZeroZeroMulActionWithZeroTopologicalSpaceFilter.NeBotTopologicalSpaceContinuousSMul