Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-24 20:12 a04c7e20

View on Github →

feat(analysis/topology): miscellaneous topology (#484)

  • miscellaneous topology
  • C is a proper metric space
  • Sum of metric spaces is a def instead of instance
  • refactor(analysis): shorten/simplify proofs

Estimated changes

deleted theorem bdd_above_Int1
deleted theorem bdd_above_Int2
modified theorem bdd_above_empty
modified theorem bdd_above_finite
modified theorem bdd_above_finite_union
added theorem bdd_above_inter_left
added theorem bdd_above_inter_right
deleted theorem bdd_below_Int1
deleted theorem bdd_below_Int2
modified theorem bdd_below_empty
modified theorem bdd_below_finite
modified theorem bdd_below_finite_union
added theorem bdd_below_inter_left
added theorem bdd_below_inter_right
deleted theorem lattice.cInf_of_in_of_le
deleted theorem lattice.cSup_of_in_of_le
added theorem lattice.cinfi_le
added theorem lattice.cinfi_le_cinfi
added theorem lattice.csupr_le
added theorem lattice.csupr_le_csupr
added theorem lattice.is_glb_cInf
added theorem lattice.is_lub_cSup
added theorem lattice.le_cinfi
added theorem lattice.le_csupr