Documentation

Mathlib.Dynamics.FixedPoints.Support

Support of a self-map #

Given a self-map f : X → X of a topological space X, the closure of the non-fixed points of f is often called the support of f. Since the word "support" is used to label various concepts throughout mathematics, we will use the term "fixed support" for the concept described above. This file contains basic definitions and API for the fixed support.

source
def Function.fixedSupport {X : Type u_1} [TopologicalSpace X] (f : X → X) :
Set X

The fixed support of a self-map f : X → X is the closure of the set of non-fixed points, often called the support of f, but we use the term "fixed support" to disamiguate from other notions.

Equations
Instances For
    source
    theorem Function.fixedSupport_def {X : Type u_1} [TopologicalSpace X] (f : X → X) :
    fixedSupport f = closure (fixedPoints f)ᶜ
    source
    def Function.HasCompactFixedSupport {X : Type u_1} [TopologicalSpace X] (f : X → X) :
    Prop

    A self-map f : X → X has compact fixed support if its fixed support is compact.

    Equations
    Instances For
      source
      theorem Function.HasCompactFixedSupport_iff' {X : Type u_1} [TopologicalSpace X] {f : X → X} :
      HasCompactFixedSupport f ↔ ∃ (K : Set X), IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

      A self-map f : X → X has compact fixed support if and only if f fixes the complement of a closed compact set. If X is preregular, then use compactSupport_iff instead.

      source
      theorem Function.HasCompactFixedSupport_iff {X : Type u_1} [TopologicalSpace X] {f : X → X} [R1Space X] :
      HasCompactFixedSupport f ↔ ∃ (K : Set X), IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

      A self-map f : X → X of a preregular space X has compact fixed support if and only if f fixes the complement of a compact set.

      source
      theorem Function.hasCompactFixedSupport_id (X : Type u_1) [TopologicalSpace X] :
      HasCompactFixedSupport id
      source
      theorem Function.HasCompactFixedSupport.comp {X : Type u_1} [TopologicalSpace X] {f g : X → X} (hf : HasCompactFixedSupport f) (hg : HasCompactFixedSupport g) :
      HasCompactFixedSupport (f ∘ g)

      If f and g have compact fixed support, then so does their composition f ∘ g.

      source
      theorem Function.HasCompactFixedSupport.symm {X : Type u_1} [TopologicalSpace X] {f : X ≃ X} (hf : HasCompactFixedSupport ⇑f) :
      HasCompactFixedSupport ⇑f.symm