Skip to content

Pull requests: felixpernegger/pibase-lean

New pull request New
27 Open 39 Closed
27 Open 39 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat: prove T347, a group topology makes the space homogeneous
#1345 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T603, separable implies density at most 𝔠
#1344 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T604, cardinality at most 𝔠 implies density at most 𝔠
#1343 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T414, sequentially discrete implies US
#1342 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T226, US implies T₁
#1341 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T299, finite implies countably many continuous self-maps
#1340 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T297, countably many continuous self-maps implies countable
#1339 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T349, indiscrete implies homogeneous
#1338 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T633, homogeneity plus a closed point gives T₁
#1337 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T209, an isolated point plus homogeneity gives a discrete space
#1336 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T313, hyperconnected implies the countable chain condition
#1335 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T597, hyperconnected with an isolated point gives a generic point
#1334 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T593, a generic point makes the space hyperconnected
#1333 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T592, a generic point makes the space separable
#1332 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T259, countable implies a countable network
#1331 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T218, discrete implies locally finite
#1330 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T238, countable implies locally countable
#1329 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T757, the empty space is locally 1-Euclidean
#1328 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T138, cardinality 𝔠 is not less than 𝔠
#1327 opened Sep 12, 2026 by kisonecat Loading…
1
feat: prove T669, metrizable implies monotonically normal
#1326 opened Sep 12, 2026 by kisonecat Loading…
1
compare theorem statements between this repo and the π-base
#1325 opened Sep 12, 2026 by kisonecat Loading…
fix: make the positive implication target auditable
#1322 opened Aug 29, 2026 by Deicyde Contributor • Draft
fix: replace vacuous independence predicate
#1321 opened Aug 29, 2026 by Deicyde Contributor Loading…
1
Add audited pilot spaces and publish them on the website
#1320 opened Aug 29, 2026 by Deicyde Contributor • Draft
1
Add a Lean-native registry for Pi-Base spaces
#1319 opened Aug 28, 2026 by Deicyde Contributor Loading…
ProTip! Type g i on any issue or pull request to go back to the issue listing page.