Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-18 09:23 bec46afd

View on Github →

refactor(topology/*): use dot notation with compact, prove compact.image with continuous_on (#1809)

  • refactor(topology/*): use dot notation, prove compact.image with continuous_on
  • Apply suggestions from code review Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • Fix compile, update some proofs
  • Make range_quot_mk a simp lemma
  • Fix lint errors

Estimated changes

added theorem set.range_quot_mk
modified theorem filter.comap_mono
modified theorem filter.map_inf
added theorem filter.map_inf_le
modified theorem filter.map_mono
deleted theorem filter.monotone_comap
deleted theorem filter.monotone_map
added theorem filter.tendsto.inf
added theorem filter.tendsto.ne_bot
added theorem compact.image
added theorem compact.inter_left
added theorem compact.inter_right
added theorem compact.prod
added theorem compact.union
added theorem compact_Union
deleted theorem compact_Union_of_compact
deleted theorem compact_adherence_nhdset
deleted theorem compact_bUnion_of_compact
deleted theorem compact_image
deleted theorem compact_inter
deleted theorem compact_of_closed
deleted theorem compact_of_finite
deleted theorem compact_prod
deleted theorem compact_union_of_compact
added theorem is_closed.compact
added theorem set.finite.compact