Fixed point #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This module defines a generic
fix operator for defining recursive
computations that are not necessarily well-founded or productive.
An instance is defined for
Main definition #
has_fix α gives us a way to calculate the fixed point
of function of type
α → α.
Instances of this typeclass
Instances of other typeclasses for
A series of successive, finite approximation of the fixed point of
f, defined by
approx f n = f^[n] ⊥. The limit of this chain is the fixed point of
loop body for finding the fixed point of
The least fixed point of
f is a continuous function (according to complete partial orders),
it satisfies the equations:
fix f = f (fix f) (is a fixed point)
∀ X, f X ≤ X → fix f ≤ X (least fixed point)