theorem Fixpoint.fixpoint_of_preFixpoint_and_postFixpoint {α : Type u_1} {f : α → α} {x : α} [ha : CompleteLattice α] (h₁ : PreFixpoint f x) (h₂ : PostFixpoint f x) : Fixpoint f x

theorem Fixpoint.preFixpoint_of_fixpoint {α : Type u_1} {f : α → α} {x : α} [ha : CompleteLattice α] (h : Fixpoint f x) : PreFixpoint f x

theorem Fixpoint.postFixpoint_of_fixpoint {α : Type u_1} {f : α → α} {x : α} [ha : CompleteLattice α] (h : Fixpoint f x) : PostFixpoint f x

theorem Fixpoint.fixpoint_iff_preFixpoint_and_postFixpoint {α : Type u_1} {f : α → α} {x : α} [ha : CompleteLattice α] : Fixpoint f x ↔ PreFixpoint f x ∧ PostFixpoint f x