Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 18:15 35ef7700

View on Github →

refactor(topology/compacts): Turn into structures, use set_like, cleanup (#12035)

  • Change closeds, compacts, nonempty_compacts, positive_compacts from subtype to structure
  • Use set_like
  • Add missing instances
    • the lattice and bounded_order instances for closeds
    • the bounded_order instance for compacts
    • the semilattice_sup and order_top instances for nonempty_compacts
    • the inhabited, semilattice_sup and order_top instances for positive_compacts
  • kill positive_compacts_univ in favor of using the new order_top instance
  • rename nonempty_positive_compacts to positive_compacts.nonempty
  • sectioning the file

Estimated changes

added structure topological_space.closeds