Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-19 08:17 0087c2ce

View on Github →

feat(analysis/topology): quotient spaces and quotient maps (#155)

  • style(analysis/topology): simplify induced_mono and induced_sup
  • style(analysis/topology/topological_space): reorganize section constructions
  • feat(analysis/topology/topological_space): add more galois connection lemmas
  • feat(analysis/topology): quotient spaces and quotient maps

Estimated changes

added theorem coinduced_compose
added theorem coinduced_id
added theorem continuous_quot_lift
added theorem continuous_quot_mk
added theorem continuous_quotient_mk
deleted theorem induced_mono
deleted theorem induced_sup
added def quotient_map
added theorem quotient_map_compose
added theorem quotient_map_id
added theorem quotient_map_quot_mk
added theorem coinduced_inf
added theorem coinduced_infi
added theorem coinduced_mono
added theorem coinduced_top
added theorem gc_induced_coinduced
added theorem induced_bot
added theorem induced_mono
added theorem induced_sup
added theorem induced_supr