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

added theorem closed_ball_Icc
added def metric_space_sum
added theorem prod.dist_eq
added theorem sum.one_dist_le'
added theorem sum.one_dist_le
deleted theorem compact_of_closed
added theorem compact_prod
deleted theorem compact_univ
added theorem compact_of_closed
added theorem compact_univ
added theorem Inf_mem_closure
added theorem Inf_mem_of_is_closed
added theorem Sup_mem_closure
added theorem Sup_mem_of_is_closed
added theorem bdd_above_of_compact
added theorem bdd_below_of_compact
added theorem cInf_mem_closure
added theorem cInf_mem_of_is_closed
added theorem cSup_mem_closure
added theorem cSup_mem_of_is_closed
added theorem mem_closure_of_is_glb
added theorem mem_closure_of_is_lub
added theorem sum.uniformity
deleted theorem set.image_eq_empty
added theorem set.image_eq_empty
added theorem set.range_eq_empty
added theorem set.univ_eq_empty_iff
added theorem set.univ_ne_empty
added theorem set.finite_univ
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