Commit 2023-12-20 19:25 58d258cf

View on Github →

feat(Filter/{NAry,Pointwise}): add missing NeBot instances (#9055)

  • Add missing Filter.NeBot instances for Filter.map₂ and pointwise operations, rename Filter.prod_neBot' to Filter.prod.instNeBot.
  • Make Filter.prod_eq_bot a simp lemma.
  • Protect some lemmas.
  • Golf some proofs.
  • Make Filter.map₂_left and Filter.map₂_right take NeBot argument as an instance.

Estimated changes

deleted theorem Filter.NeBot.map₂
modified theorem Filter.NeBot.of_map₂_left
modified theorem Filter.map₂_bot_left
modified theorem Filter.map₂_bot_right
modified theorem Filter.map₂_eq_bot_iff
modified theorem Filter.map₂_left
modified theorem Filter.map₂_neBot_iff
modified theorem Filter.map₂_pure_left
modified theorem Filter.map₂_pure_right
modified theorem Filter.map₂_right
modified def Filter.map₃
deleted theorem Filter.NeBot.div
deleted theorem Filter.NeBot.inv
deleted theorem Filter.NeBot.mul
deleted theorem Filter.NeBot.smul
deleted theorem Filter.NeBot.vsub
added theorem Filter.div.instNeBot
added theorem Filter.inv.instNeBot
added theorem Filter.smul.instNeBot
added theorem Filter.vsub.instNeBot
deleted theorem Filter.NeBot.prod