Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-12 04:06 1b0a7493

View on Github →

feat(topology): is_closed_proj_of_compact (#2069)

  • feat(lattice): add inf_le_inf_left/right
  • feat(set/lattice): image_inter_subset
  • feat(set/lattice): push_pull
  • feat(order/filter): push_pull and product notation
  • feat(topology/subset_properties): is_closed_proj_of_compact
  • feat(set/lattice): push_pull'
  • fix(order/filter): forgotten doc
  • lint (including old missing docstrings in filter).
  • Apply Yury's suggestions.
  • Forgotten style fix
  • urkud's suggestions Co-Authored-By: Yury G. Kudryashov urkud@urkud.name
  • Update src/order/filter/basic.lean Co-Authored-By: Scott Morrison scott@tqft.net

Estimated changes

added theorem set.image_inter_subset
deleted theorem set.mono_image
modified theorem filter.bot_prod
added theorem filter.map_ne_bot_iff
modified theorem filter.prod_bot
modified theorem filter.prod_comm'
modified theorem filter.prod_comm
modified theorem filter.prod_eq_bot
modified theorem filter.prod_ne_bot
modified theorem filter.prod_pure_pure
modified theorem filter.tendsto_fst
modified theorem filter.tendsto_snd