Theorems · Theorem · general topology

ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self

∀ (Γ : Type u_4) {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : SMul Γ T] [ProperlyDiscontinuousSMul Γ T]
  [T2Space T] [LocallyCompactSpace T] [ContinuousConstSMul Γ T] (x : T),
  ∃ U ∈ nhds x, ∀ (γ : Γ), ((fun x => γ • x) '' U ∩ U).Nonempty → γ • x = x

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSMulProperlyDiscontinuousSMulT2SpaceLocallyCompactSpaceContinuousConstSMul