def Fixpoint.PreFixpoint {α : Type u_1} [LE α] (f : α → α) (x : α) : Prop

Equations

• Fixpoint.PreFixpoint f x = (f x ≤ x)

def Fixpoint.PostFixpoint {α : Type u_1} [LE α] (f : α → α) (x : α) : Prop

Equations

• Fixpoint.PostFixpoint f x = (x ≤ f x)

def Fixpoint.Fixpoint {α : Type u_1} (f : α → α) (x : α) : Prop

Equations

• Fixpoint.Fixpoint f x = (f x = x)