Theorems · Theorem · general topology

ProperlyDiscontinuousSMul.finite_disjoint_inter_image

∀ {Γ : Type u_4} {T : Type u_5} {inst : TopologicalSpace T} {inst_1 : SMul Γ T} [self : ProperlyDiscontinuousSMul Γ T]
  {K L : Set T}, IsCompact K → IsCompact L → {γ | ((fun x => γ • x) '' K ∩ L).Nonempty}.Finite

Given two compact sets K and L, γ • K ∩ L is nonempty for finitely many γ.

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Cited by

3 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Quot.sound

Assumes

ProperlyDiscontinuousSMul