Commit 2023-09-06 10:25 db7fecc0

View on Github →

feat: Kernel of a filter (#6981) Define the kernel of a filter as the intersection of its sets and show it forms a Galois coinsertion with the principal filter.

Estimated changes

added def Filter.ker
added theorem Filter.ker_bot
added theorem Filter.ker_comap
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