Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 10:40 8b27c457

View on Github →

feat(order/filter/pointwise): Missing pointwise operations (#13170) Define inversion/negation, division/subtraction, scalar multiplication/addition, scaling/translation, scalar subtraction of filters using the new filter.map₂. Golf the existing API.

Estimated changes

added theorem filter.bot_div
added theorem filter.bot_mul
added theorem filter.bot_smul
added theorem filter.bot_vsub
added theorem filter.div_bot
added theorem filter.div_eq_bot_iff
added theorem filter.div_mem_div
added theorem filter.div_ne_bot_iff
added theorem filter.eventually_one
added theorem filter.inv_mem_inv
added theorem filter.le_mul_iff
added theorem filter.le_one_iff
added theorem filter.le_smul_iff
added theorem filter.le_vsub_iff
added theorem filter.map_inv'
added theorem filter.map_smul
added theorem filter.map₂_div
added theorem filter.map₂_mul
added theorem filter.map₂_smul
added theorem filter.map₂_vsub
added theorem filter.mem_div
added theorem filter.mem_inv
deleted theorem filter.mem_mul
added theorem filter.mem_mul_iff
modified theorem filter.mem_one
added theorem filter.mem_smul
added theorem filter.mem_smul_filter
added theorem filter.mem_vsub
added theorem filter.mul_bot
added theorem filter.mul_eq_bot_iff
modified theorem filter.mul_mem_mul
added theorem filter.mul_ne_bot_iff
added theorem filter.ne_bot.div
added theorem filter.ne_bot.inv
modified theorem filter.ne_bot.mul
added theorem filter.ne_bot.smul
added theorem filter.ne_bot.vsub
added theorem filter.ne_bot_inv_iff
modified theorem filter.one_mem_one
added theorem filter.principal_one
added theorem filter.pure_one
added theorem filter.smul_bot
added theorem filter.smul_eq_bot_iff
added theorem filter.smul_filter_bot
added theorem filter.smul_le_smul
added theorem filter.smul_mem_smul
added theorem filter.smul_ne_bot_iff
added theorem filter.tendsto.div_div
added theorem filter.tendsto.inv_inv
added theorem filter.tendsto_one
added theorem filter.vsub_bot
added theorem filter.vsub_eq_bot_iff
added theorem filter.vsub_le_vsub
added theorem filter.vsub_mem_vsub
added theorem filter.vsub_ne_bot_iff
deleted theorem filter.map_neg