Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-09 21:53 a913b9b4

View on Github →

chore(order/filter): move filter.prod and filter.coprod to a new file (#15937) These lemmas and definitions are moved without changes.

Estimated changes

deleted theorem filter.bot_coprod
deleted theorem filter.bot_coprod_bot
deleted theorem filter.bot_prod
deleted theorem filter.comap_prod
deleted theorem filter.compl_mem_coprod
deleted theorem filter.coprod_bot
deleted theorem filter.coprod_mono
deleted theorem filter.coprod_ne_bot_iff
deleted theorem filter.coprod_ne_bot_left
deleted theorem filter.eventually.curry
deleted theorem filter.eventually.prod_mk
deleted theorem filter.map_pure_prod
deleted theorem filter.map_swap4_prod
deleted theorem filter.mem_coprod_iff
deleted theorem filter.mem_prod_iff
deleted theorem filter.mem_prod_principal
deleted theorem filter.mem_prod_top
deleted theorem filter.ne_bot.prod
deleted theorem filter.prod_assoc
deleted theorem filter.prod_assoc_symm
deleted theorem filter.prod_bot
deleted theorem filter.prod_comm'
deleted theorem filter.prod_comm
deleted theorem filter.prod_eq
deleted theorem filter.prod_eq_bot
deleted theorem filter.prod_inf_prod
deleted theorem filter.prod_infi_left
deleted theorem filter.prod_infi_right
deleted theorem filter.prod_map_map_eq'
deleted theorem filter.prod_map_map_eq
deleted theorem filter.prod_mem_prod
deleted theorem filter.prod_mem_prod_iff
deleted theorem filter.prod_mono
deleted theorem filter.prod_ne_bot
deleted theorem filter.prod_pure
deleted theorem filter.prod_pure_pure
deleted theorem filter.prod_sup
deleted theorem filter.prod_top
deleted theorem filter.pure_prod
deleted theorem filter.sup_prod
deleted theorem filter.tendsto.prod_map
deleted theorem filter.tendsto.prod_mk
deleted theorem filter.tendsto_diag
deleted theorem filter.tendsto_fst
deleted theorem filter.tendsto_prod_assoc
deleted theorem filter.tendsto_prod_iff'
deleted theorem filter.tendsto_prod_iff
deleted theorem filter.tendsto_prod_swap
deleted theorem filter.tendsto_snd
deleted theorem filter.tendsto_swap4_prod
added theorem filter.bot_coprod
added theorem filter.bot_coprod_bot
added theorem filter.bot_prod
added theorem filter.comap_prod
added theorem filter.coprod_bot
added theorem filter.coprod_mono
added theorem filter.map_pure_prod
added theorem filter.map_swap4_prod
added theorem filter.mem_coprod_iff
added theorem filter.mem_prod_iff
added theorem filter.mem_prod_top
added theorem filter.ne_bot.prod
added theorem filter.prod_assoc
added theorem filter.prod_assoc_symm
added theorem filter.prod_bot
added theorem filter.prod_comm'
added theorem filter.prod_comm
added theorem filter.prod_eq
added theorem filter.prod_eq_bot
added theorem filter.prod_inf_prod
added theorem filter.prod_infi_left
added theorem filter.prod_infi_right
added theorem filter.prod_mem_prod
added theorem filter.prod_mono
added theorem filter.prod_ne_bot
added theorem filter.prod_pure
added theorem filter.prod_pure_pure
added theorem filter.prod_sup
added theorem filter.prod_top
added theorem filter.pure_prod
added theorem filter.sup_prod
added theorem filter.tendsto.prod_mk
added theorem filter.tendsto_diag
added theorem filter.tendsto_fst
added theorem filter.tendsto_snd
added theorem filter.{u