restructureHEADmain

1 files changed, 0 insertions, 51 deletions

diff --git a/SymbolicModalLogic/FixedPoints.lean b/SymbolicModalLogic/FixedPoints.lean
deleted file mode 100644
index 58d768c..0000000
--- a/SymbolicModalLogic/FixedPoints.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-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