Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 09:50 d556d6af

View on Github →

refactor(topology/topological_space): rename open_set to opens and unbundle it (#427)

Estimated changes

Modified analysis/topology/topological_space.lean

added theorem topological_space.opens.Sup_s

added theorem topological_space.opens.ext

added def topological_space.opens.gc

added def topological_space.opens.gi

added def topological_space.opens.interior

added def topological_space.opens.is_basis

added theorem topological_space.opens.is_basis_iff_cover

added theorem topological_space.opens.is_basis_iff_nbhd

added def topological_space.opens

Modified category_theory/examples/topological_spaces.lean

added def category_theory.examples.map

added def category_theory.examples.map_id

added theorem category_theory.examples.map_id_obj

added def category_theory.examples.map_iso

added def category_theory.examples.map_iso_id

added def category_theory.examples.nbhd

added def category_theory.examples.nbhds

deleted def category_theory.examples.open_set.map

deleted def category_theory.examples.open_set.map_id

deleted theorem category_theory.examples.open_set.map_id_obj

deleted def category_theory.examples.open_set.map_iso

deleted def category_theory.examples.open_set.map_iso_id

deleted def category_theory.examples.open_set.nbhd

deleted def category_theory.examples.open_set.nbhds

deleted structure category_theory.examples.open_set