Skip to content

[Merged by Bors] - chore(Topology/Compactness/CountablyCompact): generalize theorem#39600

Closed
plp127 wants to merge 5 commits into
leanprover-community:masterfrom
plp127:aliu/inducing-free
Closed

[Merged by Bors] - chore(Topology/Compactness/CountablyCompact): generalize theorem#39600
plp127 wants to merge 5 commits into
leanprover-community:masterfrom
plp127:aliu/inducing-free

Merge branch 'master' into aliu/inducing-free

7b9b73e
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Jun 3, 2026 in 1m 18s