Commit 2023-01-30 19:30 38c52116

View on Github →

feat: port Order.Filter.Pointwise (#1839)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Pointwise.lean

added theorem Filter.NeBot.div

added theorem Filter.NeBot.div_zero_nonneg

added theorem Filter.NeBot.inv

added theorem Filter.NeBot.mul

added theorem Filter.NeBot.mul_zero_nonneg

added theorem Filter.NeBot.of_div_left

added theorem Filter.NeBot.of_div_right

added theorem Filter.NeBot.of_mul_left

added theorem Filter.NeBot.of_mul_right

added theorem Filter.NeBot.of_smul_filter

added theorem Filter.NeBot.of_smul_left

added theorem Filter.NeBot.of_smul_right

added theorem Filter.NeBot.of_vsub_left

added theorem Filter.NeBot.of_vsub_right

added theorem Filter.NeBot.one_le_div

added theorem Filter.NeBot.smul

added theorem Filter.NeBot.smul_filter

added theorem Filter.NeBot.smul_zero_nonneg

added theorem Filter.NeBot.vsub

added theorem Filter.NeBot.zero_div_nonneg

added theorem Filter.NeBot.zero_mul_nonneg

added theorem Filter.NeBot.zero_smul_nonneg

added theorem Filter.Tendsto.div_div

added theorem Filter.Tendsto.inv_inv

added theorem Filter.Tendsto.mul_mul

added theorem Filter.add_mul_subset

added theorem Filter.bot_div

added theorem Filter.bot_mul

added theorem Filter.bot_pow

added theorem Filter.bot_smul

added theorem Filter.bot_vsub

added theorem Filter.coe_pureMonoidHom

added theorem Filter.coe_pureMulHom

added theorem Filter.coe_pureOneHom

added theorem Filter.comap_mul_comap_le

added theorem Filter.div_bot

added theorem Filter.div_eq_bot_iff

added theorem Filter.div_mem_div

added theorem Filter.div_neBot_iff

added theorem Filter.div_pure

added theorem Filter.eventually_one

added theorem Filter.inv_eq_bot_iff

added theorem Filter.inv_le_iff_le_inv

added theorem Filter.inv_le_self

added theorem Filter.inv_mem_inv

added theorem Filter.inv_pure

added theorem Filter.isUnit_iff

added theorem Filter.isUnit_iff_singleton

added theorem Filter.isUnit_pure

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 def Filter.mapMonoidHom

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

added theorem Filter.mem_mul

added theorem Filter.mem_one

added theorem Filter.mem_smul

added theorem Filter.mem_smul_filter

added theorem Filter.mem_vsub

added theorem Filter.mul_add_subset

added theorem Filter.mul_bot

added theorem Filter.mul_eq_bot_iff

added theorem Filter.mul_mem_mul

added theorem Filter.mul_neBot_iff

added theorem Filter.mul_pure

added theorem Filter.mul_top_of_one_le

added theorem Filter.neBot_inv_iff

added theorem Filter.not_one_le_div_iff

added theorem Filter.nsmul_top

added theorem Filter.one_mem_one

added theorem Filter.one_neBot

added theorem Filter.one_prod_one

added theorem Filter.pow_mem_pow

added theorem Filter.principal_one

added def Filter.pureMonoidHom

added theorem Filter.pureMonoidHom_apply

added def Filter.pureMulHom

added theorem Filter.pureMulHom_apply

added def Filter.pureOneHom

added theorem Filter.pureOneHom_apply

added theorem Filter.pure_div

added theorem Filter.pure_div_pure

added theorem Filter.pure_mul

added theorem Filter.pure_mul_pure

added theorem Filter.pure_one

added theorem Filter.pure_smul

added theorem Filter.pure_smul_pure

added theorem Filter.pure_vsub

added theorem Filter.pure_vsub_pure

added theorem Filter.smul_bot

added theorem Filter.smul_eq_bot_iff

added theorem Filter.smul_filter_bot

added theorem Filter.smul_filter_eq_bot_iff

added theorem Filter.smul_filter_le_smul_filter

added theorem Filter.smul_filter_neBot_iff

added theorem Filter.smul_le_smul

added theorem Filter.smul_le_smul_left

added theorem Filter.smul_le_smul_right

added theorem Filter.smul_mem_smul

added theorem Filter.smul_neBot_iff

added theorem Filter.smul_pure

added theorem Filter.smul_set_mem_smul_filter

added theorem Filter.tendsto_one

added theorem Filter.top_mul_of_one_le

added theorem Filter.top_mul_top

added theorem Filter.top_pow

added theorem Filter.vsub_bot

added theorem Filter.vsub_eq_bot_iff

added theorem Filter.vsub_le_vsub

added theorem Filter.vsub_le_vsub_left

added theorem Filter.vsub_le_vsub_right

added theorem Filter.vsub_mem_vsub

added theorem Filter.vsub_neBot_iff

added theorem Filter.vsub_pure

added theorem Filter.zero_smul_filter

added theorem Filter.zero_smul_filter_nonpos