Commit 2023-01-23 12:37 5a32630d

View on Github →

Feat: port Order.Filter.Prod (#1772)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Prod.lean

added theorem Filter.Eventually.curry

added theorem Filter.Eventually.diag_of_prod

added theorem Filter.Eventually.diag_of_prod_left

added theorem Filter.Eventually.diag_of_prod_right

added theorem Filter.Eventually.prod_inl

added theorem Filter.Eventually.prod_inr

added theorem Filter.Eventually.prod_mk

added theorem Filter.EventuallyEq.prod_map

added theorem Filter.EventuallyLe.prod_map

added theorem Filter.NeBot.prod

added theorem Filter.Tendsto.prod_map

added theorem Filter.Tendsto.prod_map_coprod

added theorem Filter.Tendsto.prod_mk

added theorem Filter.bot_coprod

added theorem Filter.bot_coprod_bot

added theorem Filter.bot_prod

added theorem Filter.comap_prod

added theorem Filter.compl_mem_coprod

added theorem Filter.coprod_bot

added theorem Filter.coprod_mono

added theorem Filter.coprod_neBot_iff

added theorem Filter.coprod_neBot_left

added theorem Filter.coprod_neBot_right

added theorem Filter.eventually_prod_iff

added theorem Filter.eventually_prod_principal_iff

added theorem Filter.eventually_swap_iff

added theorem Filter.le_prod_map_fst_snd

added theorem Filter.map_const_principal_coprod_map_id_principal

added theorem Filter.map_fst_prod

added theorem Filter.map_prod_map_const_id_principal_coprod_principal

added theorem Filter.map_prod_map_coprod_le.{u,

added theorem Filter.map_pure_prod

added theorem Filter.map_snd_prod

added theorem Filter.map_swap4_prod

added theorem Filter.mem_coprod_iff

added theorem Filter.mem_prod_iff

added theorem Filter.mem_prod_principal

added theorem Filter.mem_prod_top

added theorem Filter.principal_coprod_principal

added theorem Filter.prod_assoc

added theorem Filter.prod_assoc_symm

added theorem Filter.prod_bot

added theorem Filter.prod_comap_comap_eq.{u,

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_infᵢ_left

added theorem Filter.prod_infᵢ_right

added theorem Filter.prod_inj

added theorem Filter.prod_le_prod

added theorem Filter.prod_map_map_eq'

added theorem Filter.prod_map_map_eq.{u,

added theorem Filter.prod_mem_prod

added theorem Filter.prod_mem_prod_iff

added theorem Filter.prod_mono

added theorem Filter.prod_mono_left

added theorem Filter.prod_mono_right

added theorem Filter.prod_neBot

added theorem Filter.prod_principal_principal

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_diag

added theorem Filter.tendsto_fst

added theorem Filter.tendsto_prodAssoc

added theorem Filter.tendsto_prodAssoc_symm

added theorem Filter.tendsto_prod_iff'

added theorem Filter.tendsto_prod_iff

added theorem Filter.tendsto_prod_swap

added theorem Filter.tendsto_snd

added theorem Filter.tendsto_swap4_prod