Theorems · Theorem · general topology

ProperlyDiscontinuousSMul.exists_nhds_disjoint_image

∀ (Γ : 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, ∀ (γ : Γ), γ • x ≠ x → Disjoint ((fun x => γ • x) '' U) U

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSMulProperlyDiscontinuousSMulT2SpaceLocallyCompactSpaceContinuousConstSMul