mathlib3
refactor(topology/order): redefine `topological_space.complete_lattice`
#9573
Open
Overview
Commits
2
Changes
View On GitHub

refactor(topology/order): redefine `topological_space.complete_lattice` #9573

urkud wants to merge 2 commits into master from cl-golf
urkud
urkud chore(order/complete_lattice): golf a few proofs
ee7cef51
urkud urkud added awaiting-review
urkud urkud added awaiting-CI
urkud Snapshot
4e95f7c1
urkud urkud changed the title chore(order/complete_lattice): golf a few proofs refactor(topology/order): redefine `topological_space.complete_lattice` 4 years ago
urkud urkud removed awaiting-review
urkud urkud added WIP
kim-em kim-em removed awaiting-CI
github-actions github-actions added merge-conflict
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