Commit 2024-10-09 04:43 4191d40e

View on Github →

chore(Filter): move defs to a new file (#17552)

Estimated changes

deleted def Filter.EventuallyEq
deleted def Filter.EventuallyLE
deleted def Filter.Tendsto
deleted def Filter.bind
deleted def Filter.comap
deleted def Filter.comk
deleted theorem Filter.filter_eq
deleted theorem Filter.inter_mem
deleted def Filter.join
deleted theorem Filter.le_def
deleted def Filter.map
deleted theorem Filter.mem_bot
deleted theorem Filter.mem_comk
deleted theorem Filter.mem_copy
deleted theorem Filter.mem_join
deleted theorem Filter.mem_of_superset
deleted theorem Filter.mem_principal
deleted theorem Filter.mem_top
deleted theorem Filter.mem_top_iff_forall
deleted theorem Filter.mp_mem
deleted theorem Filter.neBot_iff
deleted def Filter.principal
deleted def Filter.seq
deleted theorem Filter.univ_mem'
deleted theorem Filter.univ_mem
deleted structure Filter
deleted def Filter.curry
added def Filter.Tendsto
added def Filter.bind
added def Filter.comap
added def Filter.comk
added def Filter.curry
added theorem Filter.filter_eq
added theorem Filter.inter_mem
added def Filter.join
added def Filter.ker
added theorem Filter.le_def
added def Filter.map
added theorem Filter.mem_bot
added theorem Filter.mem_comk
added theorem Filter.mem_copy
added theorem Filter.mem_join
added theorem Filter.mem_of_superset
added theorem Filter.mem_principal
added theorem Filter.mem_top
added theorem Filter.mp_mem
added theorem Filter.neBot_iff
added def Filter.principal
added theorem Filter.prod_eq_inf
added def Filter.seq
added theorem Filter.univ_mem'
added theorem Filter.univ_mem
added structure Filter
deleted def Filter.ker
deleted theorem Filter.prod_eq_inf