mathlib3
refactor(order/conditionally_complete_lattice): refactor definition, add constructors
#8496
Open
Overview
Commits
60
Changes
View On GitHub

refactor(order/conditionally_complete_lattice): refactor definition, add constructors #8496

urkud wants to merge 60 commits into master from ccl-Sup
urkud
urkud chore(order/complete_lattice): generalize `Sup_eq_supr'`, add lemmas
3d648292
urkud feat(algebra/ordered_group): add `order_iso.inv`
c43a153f
urkud Golf, generalize
c1ea843e
urkud Use `alias`
4b8cd419
urkud Merge branch 'Sup-eq-supr' into ccl-Sup
b25d41ac
urkud Snapshot
4436e715
urkud chore(data/int): move some lemmas from `basic` to `order`
70bb28b5
urkud Fix
d66d1df9
urkud Snapshot
f143fe88
urkud Merge branch 'int-greatest' into ccl-Sup
f2ce3413
urkud Fix
01e7204e
urkud urkud added WIP
github-actions github-actions added blocked-by-other-PR
urkud Fix
4c77a9d9
urkud Snapshot
2fe4e8e3
urkud Fix
24c5e1f3
urkud Merge branch 'int-greatest' into ccl-PRd
4d3b7264
urkud Merge branch 'order-iso-inv-neg' into ccl-PRd
0b291a8d
github-actions github-actions added merge-conflict
urkud Merge branch 'master' into ccl-PRd
ccae0ee9
urkud Merge branch 'ccl-PRd' into ccl-Sup
4d09186a
github-actions github-actions removed merge-conflict
urkud Add `nat.is_greatest_Sup`
d467fa26
urkud Fix
6643ecce
urkud More fixes
609d48e9
urkud More fixes
580fd89d
urkud Fixes
18950aca
github-actions github-actions added merge-conflict
github-actions github-actions removed blocked-by-other-PR
urkud feat(algebra/ordered_monoid): a few more `order_dual` instances
41411421
urkud Merge branch 'covconv-dual' into ccl-Sup
522cb409
urkud Cherry-pick
1b57d442
urkud Snapshot
9bdeeff5
urkud Merge branch 'covconv-dual' into reals-DRY
cb5a802c
urkud feat(order/bounds): add `is_lub_pi` and `is_glb_pi`
4c83b24d
urkud feat(algebra/bounds): a few lemmas like `bdd_above (-s) ↔ bdd_below s`
d316f741
urkud Merge branch 'lub-pi' into reals-DRY
99cdcbc4
urkud Merge branch 'alg-bounds' into reals-DRY
03011599
urkud Update
a5dc19b6
urkud Snapshot
2b4ae012
urkud Merge branch 'alg-bounds' into reals-DRY
599143fc
urkud Update src/algebra/bounds.lean
a72aa56c
urkud Fix compile
089f5315
urkud Fix compile
d84361b2
urkud Fix
0586e31a
urkud Fix
19a745b8
urkud Merge branch 'alg-bounds' into reals-DRY
66132bfa
urkud Merge branch 'master' into reals-DRY
d6df6d00
urkud Fix compile
d5e9e763
urkud Merge branch 'master' into ccl-Sup
ee69dafd
urkud Merge branch 'reals-DRY' into ccl-Sup
7d1d674d
github-actions github-actions removed merge-conflict
urkud Fix, minor golf
e5c8684b
github-actions github-actions added merge-conflict
urkud Merge branch 'reals-DRY' into ccl-Sup
7edc85e7
urkud Merge branch 'master' into ccl-Sup
699033d7
urkud Snapshot
c51ed268
github-actions github-actions removed merge-conflict
urkud Snapshot
63d082e2
urkud Cherry-pick
a87f1806
urkud Fix names
e1dc1e6a
urkud Docs
b9c6f021
github-actions github-actions added merge-conflict
urkud Merge branch 'master' into ccl-Sup
7720934f
urkud Merge branch 'inv-le-of-inv-le' into ccl-Sup
5b20d49d
urkud Snapshot
46a5a106
urkud Snapshot
74196e2b
urkud Merge branch 'master' into ccl-Sup
f9f239ab
urkud Fix whitespace
61626bd6
urkud Merge branch 'master' into ccl-Sup
bd7550db
github-actions github-actions removed merge-conflict
github-actions github-actions added merge-conflict
github-actions
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
WIP merge-conflict too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum