# Documentation

Mathlib.Topology.Algebra.ProperConstSMul

# Actions by proper maps #

In this file we define ProperConstSMul M X to be a mixin Prop-value class stating that (c • ·) is a proper map for all c.

Note that this is not the same as a proper action (not yet in Mathlib) which requires (c, x) ↦ (c • x, x) to be a proper map.

We also provide 4 instances:

• for a continuous action on a compact Hausdorff space,
• and for a continuous group action on a general space;
• for the action on X × Y;
• for the action on ∀ i, X i.
class ProperConstVAdd (M : Type u_1) (X : Type u_2) [VAdd M X] [] :
• isProperMap_vadd : ∀ (c : M), IsProperMap fun x => c +ᵥ x

(c +ᵥ ·) is a proper map.

A mixin typeclass saying that the (c +ᵥ ·) is a proper map for all c.

Note that this is not the same as a proper additive action (not yet in Mathlib).

Instances
class ProperConstSMul (M : Type u_1) (X : Type u_2) [SMul M X] [] :
• isProperMap_smul : ∀ (c : M), IsProperMap fun x => c x

(c • ·) is a proper map.

A mixin typeclass saying that (c • ·) is a proper map for all c.

Note that this is not the same as a proper multiplicative action (not yet in Mathlib).

Instances
theorem isProperMap_vadd {M : Type u_1} (c : M) (X : Type u_2) [VAdd M X] [] [h : ] :
IsProperMap fun x => c +ᵥ x

(c +ᵥ ·) is a proper map.

theorem isProperMap_smul {M : Type u_1} (c : M) (X : Type u_2) [SMul M X] [] [h : ] :
IsProperMap fun x => c x

(c • ·) is a proper map.

theorem IsCompact.preimage_vadd {M : Type u_1} {X : Type u_2} [VAdd M X] [] [] {s : Set X} (hs : ) (c : M) :
IsCompact ((fun x => c +ᵥ x) ⁻¹' s)

The preimage of a compact set under (c +ᵥ ·) is a compact set.

theorem IsCompact.preimage_smul {M : Type u_1} {X : Type u_2} [SMul M X] [] [] {s : Set X} (hs : ) (c : M) :
IsCompact ((fun x => c x) ⁻¹' s)

The preimage of a compact set under (c • ·) is a compact set.

theorem instProperConstVAdd.proof_1 {M : Type u_1} {X : Type u_2} [VAdd M X] [] [] [] [] :
instance instProperConstVAdd {M : Type u_1} {X : Type u_2} [VAdd M X] [] [] [] [] :
instance instProperConstSMul {M : Type u_1} {X : Type u_2} [SMul M X] [] [] [] [] :