Commit 2025-02-06 07:37 0504e9a5

View on Github →

chore: split Mathlib.Order.Filter.Basic (#21403) Split out all material about map/comap and monadic operations to a new file Filter.Map.

Estimated changes

deleted theorem Filter.Eventually.comap
deleted theorem Filter.NeBot.map
deleted theorem Filter.NeBot.of_map
deleted theorem Filter.bind_def
deleted theorem Filter.bind_inf_principal
deleted theorem Filter.bind_le
deleted theorem Filter.bind_map
deleted theorem Filter.bind_mono
deleted theorem Filter.comap_bot
deleted theorem Filter.comap_comap
deleted theorem Filter.comap_comm
deleted theorem Filter.comap_const_of_mem
deleted theorem Filter.comap_equiv_symm
deleted theorem Filter.comap_eval_neBot
deleted theorem Filter.comap_fst_neBot
deleted theorem Filter.comap_iInf
deleted theorem Filter.comap_iSup
deleted theorem Filter.comap_id'
deleted theorem Filter.comap_id
deleted theorem Filter.comap_inf
deleted theorem Filter.comap_injective
deleted theorem Filter.comap_le_comap_iff
deleted theorem Filter.comap_map
deleted theorem Filter.comap_mono
deleted theorem Filter.comap_neBot
deleted theorem Filter.comap_neBot_iff
deleted theorem Filter.comap_principal
deleted theorem Filter.comap_pure
deleted theorem Filter.comap_sSup
deleted theorem Filter.comap_snd_neBot
deleted theorem Filter.comap_sup
deleted theorem Filter.comap_top
deleted theorem Filter.compl_mem_comap
deleted theorem Filter.compl_mem_kernMap
deleted theorem Filter.disjoint_comap
deleted theorem Filter.disjoint_comap_iff
deleted theorem Filter.disjoint_map
deleted theorem Filter.disjoint_of_map
deleted theorem Filter.eventuallyEq_bind
deleted theorem Filter.eventuallyLE_bind
deleted theorem Filter.eventually_bind
deleted theorem Filter.eventually_comap
deleted theorem Filter.eventually_map
deleted theorem Filter.eventually_pure
deleted theorem Filter.frequently_comap
deleted theorem Filter.frequently_map
deleted theorem Filter.gc_comap_kernMap
deleted theorem Filter.gc_map_comap
deleted theorem Filter.image_mem_map
deleted theorem Filter.image_mem_map_iff
deleted theorem Filter.join_pure
deleted def Filter.kernMap
deleted theorem Filter.kernMap_principal
deleted theorem Filter.le_comap_map
deleted theorem Filter.le_comap_top
deleted theorem Filter.le_map
deleted theorem Filter.le_map_iff
deleted theorem Filter.le_pure_iff
deleted theorem Filter.le_seq
deleted theorem Filter.map_biInf_eq
deleted theorem Filter.map_bind
deleted theorem Filter.map_bot
deleted theorem Filter.map_comap
deleted theorem Filter.map_comap_le
deleted theorem Filter.map_comap_of_mem
deleted theorem Filter.map_comm
deleted theorem Filter.map_compose
deleted theorem Filter.map_congr
deleted theorem Filter.map_const
deleted theorem Filter.map_def
deleted theorem Filter.map_eq_bot_iff
deleted theorem Filter.map_equiv_symm
deleted theorem Filter.map_iInf_eq
deleted theorem Filter.map_iInf_le
deleted theorem Filter.map_iSup
deleted theorem Filter.map_id'
deleted theorem Filter.map_id
deleted theorem Filter.map_inf'
deleted theorem Filter.map_inf
deleted theorem Filter.map_inf_le
deleted theorem Filter.map_inj
deleted theorem Filter.map_injective
deleted theorem Filter.map_le_map_iff
deleted theorem Filter.map_map
deleted theorem Filter.map_mono
deleted theorem Filter.map_neBot_iff
deleted theorem Filter.map_principal
deleted theorem Filter.map_pure
deleted theorem Filter.map_sup
deleted theorem Filter.map_swap4_eq_comap
deleted theorem Filter.map_top
deleted theorem Filter.mem_bind'
deleted theorem Filter.mem_bind
deleted theorem Filter.mem_comap''
deleted theorem Filter.mem_comap'
deleted theorem Filter.mem_comap
deleted theorem Filter.mem_comap_iff
deleted theorem Filter.mem_comap_prod_mk
deleted theorem Filter.mem_kernMap
deleted theorem Filter.mem_map'
deleted theorem Filter.mem_map
deleted theorem Filter.mem_map_seq_iff
deleted theorem Filter.mem_seq_def
deleted theorem Filter.mem_seq_iff
deleted theorem Filter.neBot_of_comap
deleted theorem Filter.preimage_mem_comap
deleted theorem Filter.principal_bind
deleted theorem Filter.principal_subtype
deleted theorem Filter.prod_map_seq_comm
deleted theorem Filter.pure_bind
deleted theorem Filter.pure_injective
deleted theorem Filter.pure_le_principal
deleted theorem Filter.pure_seq_eq_map
deleted theorem Filter.pure_sets
deleted theorem Filter.range_mem_map
deleted theorem Filter.sInter_comap_sets
deleted theorem Filter.seq_assoc
deleted theorem Filter.seq_eq_filter_seq
deleted theorem Filter.seq_mem_seq
deleted theorem Filter.seq_mono
deleted theorem Filter.seq_pure
deleted theorem Filter.singleton_mem_pure
deleted theorem Filter.sup_bind
deleted theorem GCongr.Filter.map_le_map
added theorem Filter.NeBot.map
added theorem Filter.NeBot.of_map
added theorem Filter.bind_def
added theorem Filter.bind_le
added theorem Filter.bind_map
added theorem Filter.bind_mono
added theorem Filter.comap_bot
added theorem Filter.comap_comap
added theorem Filter.comap_comm
added theorem Filter.comap_fst_neBot
added theorem Filter.comap_iInf
added theorem Filter.comap_iSup
added theorem Filter.comap_id'
added theorem Filter.comap_id
added theorem Filter.comap_inf
added theorem Filter.comap_injective
added theorem Filter.comap_map
added theorem Filter.comap_mono
added theorem Filter.comap_neBot
added theorem Filter.comap_neBot_iff
added theorem Filter.comap_principal
added theorem Filter.comap_pure
added theorem Filter.comap_sSup
added theorem Filter.comap_snd_neBot
added theorem Filter.comap_sup
added theorem Filter.comap_top
added theorem Filter.compl_mem_comap
added theorem Filter.disjoint_comap
added theorem Filter.disjoint_map
added theorem Filter.disjoint_of_map
added theorem Filter.eventually_bind
added theorem Filter.eventually_map
added theorem Filter.eventually_pure
added theorem Filter.frequently_map
added theorem Filter.gc_map_comap
added theorem Filter.image_mem_map
added theorem Filter.join_pure
added def Filter.kernMap
added theorem Filter.le_comap_map
added theorem Filter.le_comap_top
added theorem Filter.le_map
added theorem Filter.le_map_iff
added theorem Filter.le_pure_iff
added theorem Filter.le_seq
added theorem Filter.map_biInf_eq
added theorem Filter.map_bind
added theorem Filter.map_bot
added theorem Filter.map_comap
added theorem Filter.map_comap_le
added theorem Filter.map_comm
added theorem Filter.map_compose
added theorem Filter.map_congr
added theorem Filter.map_const
added theorem Filter.map_def
added theorem Filter.map_eq_bot_iff
added theorem Filter.map_equiv_symm
added theorem Filter.map_iInf_eq
added theorem Filter.map_iInf_le
added theorem Filter.map_iSup
added theorem Filter.map_id'
added theorem Filter.map_id
added theorem Filter.map_inf'
added theorem Filter.map_inf
added theorem Filter.map_inf_le
added theorem Filter.map_inj
added theorem Filter.map_injective
added theorem Filter.map_le_map_iff
added theorem Filter.map_map
added theorem Filter.map_mono
added theorem Filter.map_neBot_iff
added theorem Filter.map_principal
added theorem Filter.map_pure
added theorem Filter.map_sup
added theorem Filter.map_top
added theorem Filter.mem_bind'
added theorem Filter.mem_bind
added theorem Filter.mem_comap''
added theorem Filter.mem_comap'
added theorem Filter.mem_comap
added theorem Filter.mem_comap_iff
added theorem Filter.mem_kernMap
added theorem Filter.mem_map'
added theorem Filter.mem_map
added theorem Filter.mem_map_seq_iff
added theorem Filter.mem_seq_def
added theorem Filter.mem_seq_iff
added theorem Filter.neBot_of_comap
added theorem Filter.principal_bind
added theorem Filter.pure_bind
added theorem Filter.pure_injective
added theorem Filter.pure_seq_eq_map
added theorem Filter.pure_sets
added theorem Filter.range_mem_map
added theorem Filter.seq_assoc
added theorem Filter.seq_mem_seq
added theorem Filter.seq_mono
added theorem Filter.seq_pure
added theorem Filter.sup_bind