Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 00:17 ec9d5204

View on Github →

feat(order/filter,*): lemmas about filter.ne_bot (#9234)

  • add prod.range_fst, prod.range_snd, set.range_eval;
  • add function.surjective_eval;
  • add filter.*_ne_bot and/or filter.*_ne_bot_iff lemmas for sup, supr, comap prod.fst _, comap prod.snd _, coprod, Coprod.

Estimated changes

added theorem prod.range_fst
added theorem prod.range_snd
added theorem set.range_eval
added theorem filter.Coprod_ne_bot
added theorem filter.ne_bot.Coprod
added theorem filter.sup_ne_bot
added theorem filter.supr_ne_bot