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] [TopologicalSpace X] : Prop

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).

• isProperMap_vadd : ∀ (c : M), IsProperMap fun (x : X) => c +ᵥ x

  (c +ᵥ ·) is a proper map.

theorem ProperConstVAdd.isProperMap_vadd {M : Type u_1} {X : Type u_2} [VAdd M X] [TopologicalSpace X] [self : ProperConstVAdd M X] (c : M) : IsProperMap fun (x : X) => c +ᵥ x

(c +ᵥ ·) is a proper map.

class ProperConstSMul (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace X] : Prop

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).

• isProperMap_smul : ∀ (c : M), IsProperMap fun (x : X) => c • x

  (c • ·) is a proper map.

theorem ProperConstSMul.isProperMap_smul {M : Type u_1} {X : Type u_2} [SMul M X] [TopologicalSpace X] [self : ProperConstSMul M X] (c : M) : IsProperMap fun (x : X) => c • x

(c • ·) is a proper map.

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

(c +ᵥ ·) is a proper map.

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

(c • ·) is a proper map.

theorem IsCompact.preimage_vadd {M : Type u_1} {X : Type u_2} [VAdd M X] [TopologicalSpace X] [ProperConstVAdd M X] {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((fun (x : 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] [TopologicalSpace X] [ProperConstSMul M X] {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((fun (x : X) => c • x) ⁻¹' s)

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

@[instance 100]

instance instProperConstVAddOfContinuousConstVAddOfT2SpaceOfCompactSpace {M : Type u_1} {X : Type u_2} [VAdd M X] [TopologicalSpace X] [ContinuousConstVAdd M X] [T2Space X] [CompactSpace X] : ProperConstVAdd M X

Equations

• ⋯ = ⋯

@[instance 100]

instance instProperConstSMulOfContinuousConstSMulOfT2SpaceOfCompactSpace {M : Type u_1} {X : Type u_2} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X] [T2Space X] [CompactSpace X] : ProperConstSMul M X

Equations

• ⋯ = ⋯

@[instance 100]

instance instProperConstVAddOfContinuousConstVAdd {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace X] [ContinuousConstVAdd G X] : ProperConstVAdd G X

Equations

• ⋯ = ⋯

@[instance 100]

instance instProperConstSMulOfContinuousConstSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] : ProperConstSMul G X

Equations

• ⋯ = ⋯

instance instProperConstSMulProd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [SMul M X] [TopologicalSpace X] [ProperConstSMul M X] [SMul M Y] [TopologicalSpace Y] [ProperConstSMul M Y] : ProperConstSMul M (X × Y)

Equations

• ⋯ = ⋯

instance instProperConstSMulForall {M : Type u_1} {ι : Type u_2} {X : ι → Type u_3} [(i : ι) → SMul M (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), ProperConstSMul M (X i)] : ProperConstSMul M ((i : ι) → X i)

Equations

• ⋯ = ⋯