[Merged by Bors] - feat: define ProperConstSMul

Mathlib.lean

@@ -3125,6 +3125,7 @@ import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable
 import Mathlib.Topology.Algebra.Affine
 import Mathlib.Topology.Algebra.Algebra
+import Mathlib.Topology.Algebra.CocompactSMul
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions
 import Mathlib.Topology.Algebra.ContinuousAffineMap

Mathlib/Topology/Algebra/CocompactSMul.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.Algebra.ConstMulAction
+/-!
+# Cocompact actions
+
+In this file we define `CocompactSMul M X` to be a mixin `Prop`-value class
+stating that the preimage of a compact set under `(c • ·)` is a compact set.
+
+We also provide 2 instances:
+- for a continuous action on a compact Hausdorff space,
+- and for a continuous group action on a general space.
+-/
+
+/-- A mixin typeclass saying that
+the preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
+class CocompactVAdd (M X : Type*) [VAdd M X] [TopologicalSpace X] : Prop where
+  /-- The preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
+  isCompact_preimage_vadd (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c +ᵥ ·) ⁻¹' s)
+
+/-- A mixin typeclass saying that the preimage of a compact set under `(c • ·)` is a compact set. -/
+@[to_additive]
+class CocompactSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where
+  /-- The preimage of a compact set under `(c • ·)` is a compact set. -/
+  isCompact_preimage_smul (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c • ·) ⁻¹' s)
+
+/-- The preimage of a compact set under `(c • ·)` is a compact set. -/
+@[to_additive "The preimage of a compact set under `(c +ᵥ ·)` is a compact set."]
+theorem IsCompact.preimage_smul {M X : Type*} [SMul M X] [TopologicalSpace X] [CocompactSMul M X]
+    {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((c • ·) ⁻¹' s) :=
+  CocompactSMul.isCompact_preimage_smul c hs
+
+@[to_additive]
+instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X]
+    [T2Space X] [CompactSpace X] : CocompactSMul M X :=
+  ⟨fun c _s hs ↦ hs.preimage_continuous (continuous_const_smul c)⟩
+
+@[to_additive]
+instance (priority := 100) {G X : Type*} [Group G] [MulAction G X] [TopologicalSpace X]
+    [ContinuousConstSMul G X] : CocompactSMul G X :=
+  ⟨fun c _s hs ↦ by rw [Set.preimage_smul]; exact hs.smul _⟩

Mathlib/Topology/Separation.lean

@@ -1311,6 +1311,10 @@ theorem Bornology.relativelyCompact_eq_inCompact [T2Space α] :
   Bornology.ext _ _ Filter.coclosedCompact_eq_cocompact
 #align bornology.relatively_compact_eq_in_compact Bornology.relativelyCompact_eq_inCompact
 
+theorem IsCompact.preimage_continuous [CompactSpace α] [T2Space β] {f : α → β} {s : Set β}
+    (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s) :=
+  (hs.isClosed.preimage hf).isCompact
+
 /-- If `V : ι → Set α` is a decreasing family of compact sets then any neighborhood of
 `⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhds_of_isCompact'` where we
 don't need to assume each `V i` closed because it follows from compactness since `α` is