feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system#25900

Closed

pfaffelh wants to merge 129 commits intoleanprover-community:masterfrom

pfaffelh:pfaffelh_compactSystem3

Commits on Aug 19, 2025

started compactsystems
pfaffelh
committed
not there for compact

pfaffelh
authored and
pfaffelh
committed
not done yet

pfaffelh
authored and
pfaffelh
committed
found emptyset
pfaffelh
committed
added mono

pfaffelh
authored and
pfaffelh
committed
compiles

pfaffelh
authored and
pfaffelh
committed
dissipate
pfaffelh
committed
added dissipate

pfaffelh
authored and
pfaffelh
committed
small update

pfaffelh
authored and
pfaffelh
committed
cleaning

pfaffelh
authored and
pfaffelh
committed
cleaning2

pfaffelh
authored and
pfaffelh
committed
cleaning3

pfaffelh
authored and
pfaffelh
committed
added mono from diss
pfaffelh
committed
diss
pfaffelh
committed
final?
pfaffelh
committed
merge master
pfaffelh
committed
added or univ
pfaffelh
committed
in line with pfaffelh_compactSystem2
pfaffelh
committed
added iff

pfaffelh
authored and
pfaffelh
committed
n

pfaffelh
authored and
pfaffelh
committed
update Mathlib
pfaffelh
committed
linters dissipate
pfaffelh
committed
run mk_all

pfaffelh
authored and
pfaffelh
committed
min imports

pfaffelh
authored and
pfaffelh
committed
deleted hash
pfaffelh
committed
cs0
pfaffelh
committed
fininsh?
pfaffelh
committed
repair dissipate
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
fix two typos
pfaffelh
committed
mk_all
pfaffelh
committed
no issues
pfaffelh
committed
review dissipate
pfaffelh
committed

Commits on Aug 20, 2025

simp normal form at dissipate
pfaffelh
committed
update mathlib
pfaffelh
committed
started compact2
pfaffelh
committed
update squareCylinder
pfaffelh
committed
compactClosedSquareCylinders are a compact system
pfaffelh
committed
update Mathlib
pfaffelh
committed
deleted a comment
pfaffelh
committed
run mk_all

pfaffelh
authored and
pfaffelh
committed
merge cs
pfaffelh
committed
deleted double thm
pfaffelh
committed
small
pfaffelh
committed
sq
pfaffelh
committed
need univ
pfaffelh
committed
Revert "need univ"
pfaffelh
committed
Revert "sq"
pfaffelh
committed
more general pi
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
changed deprecated
pfaffelh
committed
rebase
pfaffelh
committed

Commits on Aug 21, 2025

space
pfaffelh
committed
started compact2
pfaffelh
committed
update squareCylinder
pfaffelh
committed
compactClosedSquareCylinders are a compact system
pfaffelh
committed
not finished with compactUnion
pfaffelh
committed
small progress
pfaffelh
committed
improve
pfaffelh
committed
transfer

pfaffelh
authored and
pfaffelh
committed
finished zero case
pfaffelh
committed
transfer2

pfaffelh
authored and
pfaffelh
committed
deleted several examples
pfaffelh
committed
almost...
pfaffelh
committed
main works

pfaffelh
authored and
pfaffelh
committed
define union

pfaffelh
authored and
pfaffelh
committed
progress

pfaffelh
authored and
pfaffelh
committed
no problems anymore
pfaffelh
committed
typos
pfaffelh
committed
update Mathlib
pfaffelh
committed
typo
pfaffelh
committed
deleted copy
pfaffelh
committed
typo
pfaffelh
committed
run mk_all

pfaffelh
authored and
pfaffelh
committed
merge cs
pfaffelh
committed
added Nat
pfaffelh
committed
deleted double thm
pfaffelh
committed
added docstring union
pfaffelh
committed
added prefixINduction

pfaffelh
authored and
pfaffelh
committed
halfway

pfaffelh
authored and
pfaffelh
committed
small
pfaffelh
committed
sq
pfaffelh
committed
Revert "sq"
pfaffelh
committed
runs half

pfaffelh
authored and
pfaffelh
committed
reworked recursion

pfaffelh
authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
Update Mathlib.lean

authored and
pfaffelh
committed
fix namespaces
pfaffelh
committed
no errors
pfaffelh
committed
no errors2
pfaffelh
committed
no errors3
pfaffelh
committed
compiles
pfaffelh
committed