feat(order/succ_pred/limit): predecessor from a `succ_order` #15614
vihdzp
wants to merge
30 commits into
master
from
is_succ_limit_pred'
start
a77ecdbe
define succ limits
0b6d4e7d
pred
f1510173
more lemmas
ba4fb58f
more lemmas
e0c935b9
Update basic.lean
3d9a9160
done!
87ca216c
simp
3687dcce
extra lemmas
ba88f083
half fix
23ad2d9c
tweak more
24c236a2
Update basic.lean
2c769488
better recursors
a233d182
Update basic.lean
60b8f66e
tweak vars
f8199958
reorder arguments of eliminators
bdafcfa5
fix name
af235402
move file
e1fd4da8
Update limit.lean
90502504
fixes
afc1051e
tweak archimedean lemmas
75dbc52f
Merge branch 'is_succ_limit' into is_succ_limit_pred'
2b941413
let's go
1bd68643
Merge branch 'master' into is_succ_limit_pred'
07f6719a
Update limit.lean
e664113b
instance → def
3569db85
golf instances
3463e311
Update limit.lean
7d7d1cf1
add lemma + golf
b0db584f
fix
4817e288
YaelDillies
commented
on 2022-07-23
Login to write a write a comment.
Login via GitHub