order): complete lattice of bornologies, generated bornology
#12964

Open

feat(topology/bornology/order): complete lattice of bornologies, generated bornology #12964

ADedecker wants to merge 5 commits into master from bornology_order

Begin

ebdd3b5c

Finished?

5291091e

Finished!

10ff0c3e

Module docstring

36139b0a

ADedecker added awaiting-review

ADedecker added awaiting-CI

ADedecker requested a review from

j-loreaux 3 years ago

ADedecker requested a review from

YaelDillies 3 years ago

YaelDillies commented on 2022-03-26

github-actions removed awaiting-CI

Yael's suggestions

04fab1fc

leanprover-community-bot-assistant added merge-conflict

ADedecker removed awaiting-review

ADedecker added WIP

kim-em added too-late

Reviewers

PatrickMassot

YaelDillies

j-loreaux

Assignees

No one assigned

Labels

WIP merge-conflict too-late

Milestone

No milestone