-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Create Knaster_Tarski.lean #88
Conversation
variables (f : α → α) (M : monotone f) | ||
|
||
def fixed_points : set α := { x | f x = x } | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess you want a lemma:
lemma fixed_points.eq {x} (h : x \in fixed_points f M) : f x = x := h
and use .2.eq
this instead of .2
in the further proofs, then you can use simp
and rw
..
le_antisymm | ||
(next.apply_le M) | ||
(lfp_le $ sup_le (le_trans H (M next.le)) (M $ next.apply_le M)) | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
what about def next.fixed_point {x : : α} (H : x ≤ f x) : fixed_point
(in similar for previous) then you can shorten some proofs below.
Could you do the changes for me? I get strange errors when I do them. |
Closed by 162edc3 |
Knaster--Tarski theorem: if f is an order-preserving function from a complete lattice to itself, then the fixed points of f is a complete sublattice (in particular, this implies that a fixed point exists).