Commit 2024-01-29 06:37 1da1e9e1

View on Github →

feat: minor topological improvements (#9908)

  • Prove that a set is a Gdelta if and only if it is an intersection of open sets indexed by ℕ.
  • Cleanup porting todos in the Gdelta file
  • Rename cluster_point_of_compact to exists_clusterPt_of_compactSpace
  • Generalize the class T2Space to T2OrLocallyCompactRegularSpace in the file Support.lean

Estimated changes

deleted theorem cluster_point_of_compact
modified theorem IsClosed.isGδ
modified theorem isGδ_iInter
modified theorem isGδ_iInter_of_isOpen
modified theorem isGδ_setOf_continuousAt
modified theorem HasCompactMulSupport.intro