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:

class ProperConstVAdd (M : Type u_1) (X : Type u_2) [VAdd M X] [TopologicalSpace X] :

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.

Instances
    theorem ProperConstVAdd.isProperMap_vadd {M : Type u_1} {X : Type u_2} :
    ∀ {inst : VAdd M X} {inst_1 : 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] :

    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.

    Instances
      theorem ProperConstSMul.isProperMap_smul {M : Type u_1} {X : Type u_2} :
      ∀ {inst : SMul M X} {inst_1 : 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]
      Equations
      • =
      @[instance 100]
      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] :
      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
      • =