Grace/Cumulus/FixedPoint/KnasterTarski.g17

Open in Workbench Download source

Imports

Set

Declarations

Source

1-- The Knaster–Tarski theorem on subsets: a monotone map on the power set2-- of X has a least fixed point, the intersection of its pre-fixed points,3-- and a greatest one, the union of its post-fixed points4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.FixedPoint.KnasterTarski10import Set1112predicate MonotoneOnSubsets (F X : Set) :=13  FunctionBetween(F, 𝒫(X), 𝒫(X)) ∧14  (∀ A ∈ 𝒫(X), ∀ B ∈ 𝒫(X), A ⊆ B → F(A) ⊆ F(B))1516def prefixedPoints (F X : Set) : Set := { A ∈ 𝒫(X) | F(A) ⊆ A }17def postfixedPoints (F X : Set) : Set := { A ∈ 𝒫(X) | A ⊆ F(A) }18def leastFixedPoint (F X : Set) : Set := ⋂(prefixedPoints(F, X))19def greatestFixedPoint (F X : Set) : Set := ⋃(postfixedPoints(F, X))2021theorem MonotoneOnSubsets.apply_subset (F X A : Set)22  requires monotone : MonotoneOnSubsets(F, X)23  requires hA : A ⊆ X24  shows F(A) ⊆ X25proof26  have member := powerset.membership_iff.backward with hA27  have value := FunctionBetween.apply_closed with monotone.left, member28  exact powerset.membership_iff.forward with value2930theorem MonotoneOnSubsets.monotone (F X A B : Set)31  requires monotone : MonotoneOnSubsets(F, X)32  requires hA : A ⊆ X33  requires hB : B ⊆ X34  requires hAB : A ⊆ B35  shows F(A) ⊆ F(B)36proof37  have memberA := powerset.membership_iff.backward with hA38  have memberB := powerset.membership_iff.backward with hB39  exact monotone.right with A, memberA, B, memberB, hAB4041theorem prefixedPoints.whole (F X : Set)42  requires monotone : MonotoneOnSubsets(F, X)43  shows X ∈ prefixedPoints(F, X)44proof45  apply prefixedPoints.membership.backward46  refine ⟨(powerset.self at X), ?_⟩47  exact MonotoneOnSubsets.apply_subset with monotone, (Subset.reflexive at X)4849theorem leastFixedPoint.subset (F X : Set)50  requires monotone : MonotoneOnSubsets(F, X)51  shows leastFixedPoint(F, X) ⊆ X52proof53  unfold leastFixedPoint54  exact familyIntersection.subset_of_member with (prefixedPoints.whole with monotone)5556theorem leastFixedPoint.below (F X A : Set)57  requires hA : A ⊆ X58  requires prefixed : F(A) ⊆ A59  shows leastFixedPoint(F, X) ⊆ A60proof61  have member : A ∈ prefixedPoints(F, X)62    apply prefixedPoints.membership.backward63    exact ⟨(powerset.membership_iff.backward with hA), prefixed⟩64  unfold leastFixedPoint65  exact familyIntersection.subset_of_member with member6667theorem leastFixedPoint.prefixed (F X : Set)68  requires monotone : MonotoneOnSubsets(F, X)69  shows F(leastFixedPoint(F, X)) ⊆ leastFixedPoint(F, X)70proof71  have whole := prefixedPoints.whole with monotone72  have inhabited : Nonempty(prefixedPoints(F, X)) := ⟨X, whole⟩73  have inside := leastFixedPoint.subset with monotone74  unfold leastFixedPoint at inside75  unfold leastFixedPoint76  apply familyIntersection.greatest with inhabited77  intros A hA78  have parts := prefixedPoints.membership.forward with hA79  have hAX := powerset.membership_iff.forward with parts.left80  have below := leastFixedPoint.below with hAX, parts.right81  unfold leastFixedPoint at below82  have step := MonotoneOnSubsets.monotone with monotone, inside, hAX, below83  exact Subset.transitive with step, parts.right8485theorem leastFixedPoint.fixed (F X : Set)86  requires monotone : MonotoneOnSubsets(F, X)87  shows F(leastFixedPoint(F, X)) = leastFixedPoint(F, X)88proof89  have prefixed := leastFixedPoint.prefixed with monotone90  have inside := leastFixedPoint.subset with monotone91  have imageInside := MonotoneOnSubsets.apply_subset with monotone, inside92  apply Subset.antisymmetric93  . exact prefixed94  . have step := MonotoneOnSubsets.monotone with monotone, imageInside, inside, prefixed95    exact leastFixedPoint.below with imageInside, step9697theorem leastFixedPoint.least (F X A : Set)98  requires hA : A ⊆ X99  requires fixed : F(A) = A100  shows leastFixedPoint(F, X) ⊆ A101proof102  have prefixed : F(A) ⊆ A103    rw fixed104    exact Subset.reflexive105  exact leastFixedPoint.below with hA, prefixed106107theorem greatestFixedPoint.subset (F X : Set)108  shows greatestFixedPoint(F, X) ⊆ X109proof110  unfold greatestFixedPoint111  apply union.subset112  intros A hA113  have parts := postfixedPoints.membership.forward with hA114  exact powerset.membership_iff.forward with parts.left115116theorem greatestFixedPoint.above (F X A : Set)117  requires hA : A ⊆ X118  requires postfixed : A ⊆ F(A)119  shows A ⊆ greatestFixedPoint(F, X)120proof121  have member : A ∈ postfixedPoints(F, X)122    apply postfixedPoints.membership.backward123    exact ⟨(powerset.membership_iff.backward with hA), postfixed⟩124  unfold greatestFixedPoint125  exact union.subset_of_member with member126127theorem greatestFixedPoint.postfixed (F X : Set)128  requires monotone : MonotoneOnSubsets(F, X)129  shows greatestFixedPoint(F, X) ⊆ F(greatestFixedPoint(F, X))130proof131  have inside := greatestFixedPoint.subset at F, X132  unfold greatestFixedPoint at inside133  unfold greatestFixedPoint134  apply union.subset135  intros A hA136  have parts := postfixedPoints.membership.forward with hA137  have hAX := powerset.membership_iff.forward with parts.left138  have above := greatestFixedPoint.above with hAX, parts.right139  unfold greatestFixedPoint at above140  have step := MonotoneOnSubsets.monotone with monotone, hAX, inside, above141  exact Subset.transitive with parts.right, step142143theorem greatestFixedPoint.fixed (F X : Set)144  requires monotone : MonotoneOnSubsets(F, X)145  shows F(greatestFixedPoint(F, X)) = greatestFixedPoint(F, X)146proof147  have postfixed := greatestFixedPoint.postfixed with monotone148  have inside := greatestFixedPoint.subset at F, X149  have imageInside := MonotoneOnSubsets.apply_subset with monotone, inside150  apply Subset.antisymmetric151  . have step := MonotoneOnSubsets.monotone with monotone, inside, imageInside, postfixed152    exact greatestFixedPoint.above with imageInside, step153  . exact postfixed154155theorem greatestFixedPoint.greatest (F X A : Set)156  requires hA : A ⊆ X157  requires fixed : F(A) = A158  shows A ⊆ greatestFixedPoint(F, X)159proof160  have postfixed : A ⊆ F(A)161    rw fixed162    exact Subset.reflexive163  exact greatestFixedPoint.above with hA, postfixed164165-- The theorem itself: a monotone map on the subsets of X has a fixed point.166theorem KnasterTarski.theorem (F X : Set)167  requires monotone : MonotoneOnSubsets(F, X)168  shows ∃ A, A ⊆ X ∧ F(A) = A169proof170  witness leastFixedPoint(F, X)171  exact ⟨(leastFixedPoint.subset with monotone), (leastFixedPoint.fixed with monotone)⟩172