Fixed points of a self-map
In this file we define
- the predicate
is_fixed_pt f x := f x = x; - the set
fixed_points fof fixed points of a self-mapf.
We also prove some simple lemmas about is_fixed_pt and ∘, iterate, and semiconj.
Tags
fixed point
A point x is a fixed point of f : α → α if f x = x.
Equations
- function.is_fixed_pt f x = (f x = x)
Every point is a fixed point of id.
Equations
- function.is_fixed_pt.decidable = h (f x) x
If x is a fixed point of f, then f x = x. This is useful, e.g., for rw or simp.
If x is a fixed point of f and g, then it is a fixed point of f ∘ g.
If x is a fixed point of f, then it is a fixed point of f^[n].
If x is a fixed point of f ∘ g and g, then it is a fixed point of f.
If x is a fixed point of f and g is a left inverse of f, then x is a fixed
point of g.
If g (semi)conjugates fa to fb, then it sends fixed points of fa to fixed points
of fb.
The set of fixed points of a map f : α → α.
Equations
- function.fixed_points f = {x : α | function.is_fixed_pt f x}
If g semiconjugates fa to fb, then it sends fixed points of fa to fixed points
of fb.
Any two maps f : α → β and g : β → α are inverse of each other on the sets of fixed points
of f ∘ g and g ∘ f, respectively.
Any map f sends fixed points of g ∘ f to fixed points of 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 inv_on_fixed_pts_comp.
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.inv_on_fixed_pts_comp.
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.bij_on_fixed_pts_comp.
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.bij_on_fixed_pts_comp.