Theorems · Inductive type · general topology

ProperlyDiscontinuousVAdd

(Γ : Type u_4) → (T : Type u_5) → [TopologicalSpace T] → [VAdd Γ T] → Prop

Class ProperlyDiscontinuousVAdd Γ T says that the additive action (+ᵥ) : Γ → T → T is properly discontinuous, that is, for any pair of compact sets K, L in T, only finitely many γ : Γ move K to have nontrivial intersection with L.

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Cited by

18 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceVAdd