From fe38333f3152f1757f9b85d47aec2e23b33aacce Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Tue, 14 Jul 2026 20:01:36 +0200
Subject: restructure

---
 CoalgebraicMuCalculus/FixedPoints.lean | 51 ++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)
 create mode 100644 CoalgebraicMuCalculus/FixedPoints.lean

(limited to 'CoalgebraicMuCalculus/FixedPoints.lean')

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
-- 
cgit v1.3.1