Commit 2024-01-26 13:55 1fec3c4a

View on Github →

chore(Filter/Ker): move from Filter.Basic to a new file (#10023) Start moving parts of >3K lines long Filter.Basic to new files.

Estimated changes

deleted def Filter.ker
deleted theorem Filter.ker_bot
deleted theorem Filter.ker_comap
deleted theorem Filter.ker_def
deleted theorem Filter.ker_eq_univ
deleted theorem Filter.ker_iInf
deleted theorem Filter.ker_inf
deleted theorem Filter.ker_mono
deleted theorem Filter.ker_principal
deleted theorem Filter.ker_pure
deleted theorem Filter.ker_sInf
deleted theorem Filter.ker_surjective
deleted theorem Filter.ker_top
deleted theorem Filter.mem_ker
deleted theorem Filter.subset_ker
added def Filter.ker
added theorem Filter.ker_bot
added theorem Filter.ker_comap
added theorem Filter.ker_def
added theorem Filter.ker_eq_univ
added theorem Filter.ker_iInf
added theorem Filter.ker_inf
added theorem Filter.ker_mono
added theorem Filter.ker_principal
added theorem Filter.ker_pure
added theorem Filter.ker_sInf
added theorem Filter.ker_surjective
added theorem Filter.ker_top
added theorem Filter.mem_ker
added theorem Filter.subset_ker