blob: 20749923c31f5be37885110a166bd864ba858bc1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
import Mathlib
namespace FixedPoints
variable {α : Type} [CompleteLattice α]
def lfp (f : α → α) : α := sInf { x | f x ≤ x }
def gfp (f : α → α) : α := sSup { x | x ≤ f x }
lemma lfp_isFixedPt (f : α → α) (h : Monotone f) : Function.IsFixedPt f (lfp f) := by
have hmem : f (lfp f) ≤ lfp f := by
rw [lfp, le_sInf_iff]
intro x hx
grw [h (sInf_le hx)]
exact hx
apply Std.IsPartialOrder.le_antisymm
· exact hmem
· exact (sInf_le (h hmem))
lemma lfp_is_least (f : α → α) :
∀ x, Function.IsFixedPt f x → lfp f ≤ x := by
intro x hfix
apply sInf_le
simp [show f x = x from hfix]
-- TODO: Avoid repitition
lemma gfp_isFixedPt (f : α → α) (h : Monotone f) : Function.IsFixedPt f (gfp f) := 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 h (le_sSup hx)
apply Std.IsPartialOrder.le_antisymm
· apply le_sSup
exact h hmem
· exact hmem
lemma gfp_is_greatest (f : α → α) :
∀ x, Function.IsFixedPt f x → x ≤ gfp f := by
intro x hfix
apply le_sSup
simp [show f x = x from hfix]
end FixedPoints
|
