Theorem Knaster_Tarski_fixpoint {P:Poset} (P_complete : is_complete P) (f : posetmorphism P P) {x0} (x0_postfix : x0 ≤ f x0) : least_suchthat (fun x:P => f x = x ∧ x0 ≤ x). Proof. set (is_f_closed := (fun A => (∀ y, A y ⇒ A (f y))) : hsubtype P -> hProp). set (is_sup_closed := (fun A => ∀ C' : hsubtype P, C' ⊆ A ⇒ A (P_complete C')) : hsubtype P -> hProp). set (C := (fun x => ∀ A : hsubtype P, A x0 ⇒ is_f_closed A ⇒ is_sup_closed A ⇒ A x) : hsubtype P). assert (C_x0 : C x0). { intros A A_x0 A_f_closed A_sup_closed; assumption. } assert (C_f_closed : is_f_closed C). { intros x C_x A A_x0 A_f_closed A_sup_closed. use A_f_closed. use C_x; assumption. } assert (C_sup_closed : is_sup_closed C). { intros X C_X A A_x0 A_f_closed A_sup_closed. use A_sup_closed; intros ? ?; use C_X; assumption. } assert (C_induction : ∀ (A : hsubtype P), A x0 ⇒ is_f_closed (A ∩ C) ⇒ is_sup_closed (A ∩ C) ⇒ C ⊆ A). { intros A A_x0 A_sup_closed A_f_closed x Cx. apply (Cx (fun x => A x ∧ C x)); [ split | | ]; assumption. } assert (postfix_supclosed : is_sup_closed (fun x => x ≤ f x)). { intros A A_postfix. apply least_upper_bound_subtype_univ. intros x A_x. eapply istrans_posetRelation. { use A_postfix; apply A_x. } apply posetmorphism_property. apply least_upper_bound_subtype_is_upper_bound, A_x. } assert (postfix_C : C ⊆ (fun x => x ≤ f x)). { use C_induction. - apply x0_postfix. - intros x [x_postfix C_x]. split. 2: { use C_f_closed; assumption. } apply posetmorphism_property, x_postfix. - intros A IH_A. split. 2: { use C_sup_closed; apply (istrans_subtype_containment IH_A), subtype_binaryintersection_leq2. } use postfix_supclosed. apply (istrans_subtype_containment IH_A). apply subtype_binaryintersection_leq1. } assert (C_below_allfix : ∏ x, (f x = x) ⇒ x0 ≤ x ⇒ C ⊆ (fun y => y ≤ x)). { intros x x_fix leq_x0_x. use C_induction. - assumption. - intros y [le_yx C_y]. split. 2: { use C_f_closed; assumption. } eapply istrans_posetRelation. { apply posetmorphism_property, le_yx. } apply isrefl'_posetRelation, x_fix. - intros A IH_A. split. 2: { use C_sup_closed. apply (istrans_subtype_containment IH_A), subtype_binaryintersection_leq2. } apply least_upper_bound_subtype_univ. apply (istrans_subtype_containment IH_A), subtype_binaryintersection_leq1. } set (sup_C := P_complete C). assert (C_sup_C : C sup_C). { use C_sup_closed. intros ? ?; assumption. } simple refine (((sup_C : P),,(_,,_)),,_); simpl. - apply isantisymm_posetRelation. + refine (least_upper_bound_is_upper_bound sup_C (_,,_)). use C_f_closed. apply C_sup_C. + use postfix_C. apply C_sup_C. - refine (least_upper_bound_is_upper_bound sup_C (_,,_)); assumption. - intros [x [x_fix leq_x0_x]]; simpl. apply least_upper_bound_subtype_univ, C_below_allfix; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.