# Fixed points of a self-map #

In this file we define

• the predicate IsFixedPt f x := f x = x;
• the set fixedPoints f of fixed points of a self-map f.

We also prove some simple lemmas about IsFixedPt and ∘, iterate, and Semiconj.

## Tags #

fixed point

theorem Function.isFixedPt_id {α : Type u} (x : α) :

Every point is a fixed point of id.

instance Function.IsFixedPt.decidable {α : Type u} [h : ] {f : αα} {x : α} :
Equations
• Function.IsFixedPt.decidable = h (f x) x
theorem Function.IsFixedPt.eq {α : Type u} {f : αα} {x : α} (hf : ) :
f x = x

If x is a fixed point of f, then f x = x. This is useful, e.g., for rw or simp.

theorem Function.IsFixedPt.comp {α : Type u} {f : αα} {g : αα} {x : α} (hf : ) (hg : ) :

If x is a fixed point of f and g, then it is a fixed point of f ∘ g.

theorem Function.IsFixedPt.iterate {α : Type u} {f : αα} {x : α} (hf : ) (n : ) :

If x is a fixed point of f, then it is a fixed point of f^[n].

theorem Function.IsFixedPt.left_of_comp {α : Type u} {f : αα} {g : αα} {x : α} (hfg : Function.IsFixedPt (f g) x) (hg : ) :

If x is a fixed point of f ∘ g and g, then it is a fixed point of f.

theorem Function.IsFixedPt.to_leftInverse {α : Type u} {f : αα} {g : αα} {x : α} (hf : ) (h : ) :

If x is a fixed point of f and g is a left inverse of f, then x is a fixed point of g.

theorem Function.IsFixedPt.map {α : Type u} {β : Type v} {fa : αα} {fb : ββ} {x : α} (hx : ) {g : αβ} (h : Function.Semiconj g fa fb) :

If g (semi)conjugates fa to fb, then it sends fixed points of fa to fixed points of fb.

theorem Function.IsFixedPt.apply {α : Type u} {f : αα} {x : α} (hx : ) :
theorem Function.IsFixedPt.preimage_iterate {α : Type u} {f : αα} {s : Set α} (h : ) (n : ) :
theorem Function.IsFixedPt.image_iterate {α : Type u} {f : αα} {s : Set α} (h : ) (n : ) :
theorem Function.IsFixedPt.equiv_symm {α : Type u} {x : α} {e : } (h : Function.IsFixedPt (⇑e) x) :
theorem Function.IsFixedPt.perm_inv {α : Type u} {x : α} {e : } (h : Function.IsFixedPt (⇑e) x) :
theorem Function.IsFixedPt.perm_pow {α : Type u} {x : α} {e : } (h : Function.IsFixedPt (⇑e) x) (n : ) :
Function.IsFixedPt (⇑(e ^ n)) x
theorem Function.IsFixedPt.perm_zpow {α : Type u} {x : α} {e : } (h : Function.IsFixedPt (⇑e) x) (n : ) :
Function.IsFixedPt (⇑(e ^ n)) x
@[simp]
theorem Function.Injective.isFixedPt_apply_iff {α : Type u} {f : αα} (hf : ) {x : α} :
def Function.fixedPoints {α : Type u} (f : αα) :
Set α

The set of fixed points of a map f : α → α.

Equations
• = {x : α | }
Instances For
instance Function.fixedPoints.decidable {α : Type u} [] (f : αα) (x : α) :
Equations
• = Function.IsFixedPt.decidable
@[simp]
theorem Function.mem_fixedPoints {α : Type u} {f : αα} {x : α} :
theorem Function.mem_fixedPoints_iff {α : Type u_1} {f : αα} {x : α} :
f x = x
@[simp]
theorem Function.fixedPoints_id {α : Type u} :
= Set.univ
theorem Function.fixedPoints_subset_range {α : Type u} {f : αα} :
theorem Function.Semiconj.mapsTo_fixedPoints {α : Type u} {β : Type v} {fa : αα} {fb : ββ} {g : αβ} (h : Function.Semiconj g fa fb) :

If g semiconjugates fa to fb, then it sends fixed points of fa to fixed points of fb.

theorem Function.invOn_fixedPoints_comp {α : Type u} {β : Type v} (f : αβ) (g : βα) :

Any two maps f : α → β and g : β → α are inverse of each other on the sets of fixed points of f ∘ g and g ∘ f, respectively.

theorem Function.mapsTo_fixedPoints_comp {α : Type u} {β : Type v} (f : αβ) (g : βα) :

Any map f sends fixed points of g ∘ f to fixed points of f ∘ g.

theorem Function.bijOn_fixedPoints_comp {α : Type u} {β : Type v} (f : αβ) (g : βα) :

Given two maps f : α → β and g : β → α, g is a bijective map between the fixed points of f ∘ g and the fixed points of g ∘ f. The inverse map is f, see invOn_fixedPoints_comp.

theorem Function.Commute.invOn_fixedPoints_comp {α : Type u} {f : αα} {g : αα} (h : ) :

If self-maps f and g commute, then they are inverse of each other on the set of fixed points of f ∘ g. This is a particular case of Function.invOn_fixedPoints_comp.

theorem Function.Commute.left_bijOn_fixedPoints_comp {α : Type u} {f : αα} {g : αα} (h : ) :

If self-maps f and g commute, then f is bijective on the set of fixed points of f ∘ g. This is a particular case of Function.bijOn_fixedPoints_comp.

theorem Function.Commute.right_bijOn_fixedPoints_comp {α : Type u} {f : αα} {g : αα} (h : ) :

If self-maps f and g commute, then g is bijective on the set of fixed points of f ∘ g. This is a particular case of Function.bijOn_fixedPoints_comp.