mathlib3
feat(topology/lindelof): define Lindelöf space
#11716
Open
Overview
Commits
22
Changes
View On GitHub

feat(topology/lindelof): define Lindelöf space #11716

urkud wants to merge 22 commits into master from YK-lindelof
urkud
urkud Snapshot
8ac825d4
urkud feat(order/filter/countable_Inter): review
a763de51
urkud Snapshot
38c8b7a4
urkud Merge branch 'master' into YK-lindelof
3216f1b8
urkud Fix
37e98d46
urkud Fix
579fb505
urkud Revert
93e6f878
urkud Merge branch 'YK-set-lattice' into YK-lindelof
71f7b11f
urkud Merge branch 'YK-countable-Inter' into YK-lindelof
74031c21
urkud Revert
550b39db
urkud Snapshot
d2ffced2
urkud Snapshot
b1423d35
urkud Merge branch 'master' into YK-lindelof
cf726a40
urkud Snapshot
25f56ce1
urkud urkud added awaiting-author
urkud Snapshot
a0cca9b1
urkud Add docs, lower instance priority
fe91e697
urkud Fix
65803019
urkud urkud removed awaiting-author
urkud urkud added awaiting-CI
urkud urkud added awaiting-review
github-actions github-actions removed awaiting-CI
sgouezel
sgouezel sgouezel removed awaiting-review
sgouezel sgouezel added awaiting-author
urkud Merge branch 'master' into YK-lindelof
494692ed
urkud Merge branch 'master' into YK-lindelof
ba278925
leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict
urkud Merge branch 'master' into YK-lindelof
43749449
urkud Smaller diff
8a59b507
urkud Fix
414c824a
kim-em kim-em added too-late
eric-wieser eric-wieser requested a review 2 years ago

Login to write a write a comment.

Login via GitHub

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