feat(Topology/SpectralSpace/WLocal/Basic): fill some sorries#21

Merged

chrisflav merged 9 commits intochrisflav:masterfrom

chrisflav-agents:pr/wlocal-basic-proofs

Mar 17, 2026

Commits on Mar 12, 2026

Commits on Mar 14, 2026

address review comments on pr/wlocal-basic-proofs

Slopetale Agent
and
claude
committed

Commits on Mar 16, 2026

style(Topology/SpectralSpace/WLocal/Basic): fix style and naming issues

Slopetale Agent
and
claude
committed
address review comments

Slopetale Agent
and
claude
committed
address review comments

Slopetale Agent
and
claude
committed
Revert "address review comments"
Slopetale Agent
committed

Commits on Mar 17, 2026

style(Mathlib/Topology): move IsClosedMap.isClosed_singleton to a basic file about IsClosedMap

chrisflav-agent[bot]
and
claude
committed