1 files changed, 51 insertions, 0 deletions
diff --git a/CoalgebraicMuCalculus/FixedPoints.lean b/CoalgebraicMuCalculus/FixedPoints.lean
new file mode 100644
index 0000000..58d768c
--- /dev/null
+++ b/CoalgebraicMuCalculus/FixedPoints.lean
@@ -0,0 +1,51 @@
+import Mathlib
+
+variable {α : Type} [CompleteLattice α]
+
+structure Function.IsLeastFixedPt (f : α → α) (x : α) : Prop where
+  fixedPt : Function.IsFixedPt f x
+  least : ∀ y, Function.IsFixedPt f y → x ≤ y
+
+structure Function.IsGreatestFixedPt (f : α → α) (x : α) : Prop where
+  fixedPt : Function.IsFixedPt f x
+  greatest : ∀ y, Function.IsFixedPt f y → y ≤ x
+
+namespace FixedPoints
+
+def lfp (f : α → α) : α := sInf { x | f x ≤ x }
+
+def gfp (f : α → α) : α := sSup { x | x ≤ f x }
+
+lemma lfp_isLeastFixedPt (f : α → α) (hf : Monotone f) : Function.IsLeastFixedPt f (lfp f) where
+  fixedPt := by
+    have hmem : f (lfp f) ≤ lfp f := by
+      rw [lfp, le_sInf_iff]
+      intro x hx
+      grw [hf (sInf_le hx)]
+      exact hx
+    apply Std.IsPartialOrder.le_antisymm
+    · exact hmem
+    · exact (sInf_le (hf hmem))
+  least := by
+    intro x hfix
+    apply sInf_le
+    simp [show f x = x from hfix]
+
+-- TODO: Avoid repitition
+lemma gfp_isGreatestFixedPt (f : α → α) (hf : Monotone f) : Function.IsGreatestFixedPt f (gfp f) where
+  fixedPt := by
+    have hmem : gfp f ≤ f (gfp f) := by
+      rw [gfp, sSup_le_iff]
+      intro x hx
+      grw [show x ≤ f x from hx]
+      exact hf (le_sSup hx)
+    apply Std.IsPartialOrder.le_antisymm
+    · apply le_sSup
+      exact hf hmem
+    · exact hmem
+  greatest := by
+    intro x hfix
+    apply le_sSup
+    simp [show f x = x from hfix]
+
+end FixedPoints