mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard
verified publisher icon leanprover-community

feat : define cocountable and cocardinal filters

Open JADekker opened this issue 2 years ago • 2 comments

Define cocountable and cocardinal filters.

Any feedback on the way these are phrased and written is more than welcome!

Open in Gitpod

JADekker avatar Feb 13 '24 22:02 JADekker

#10531 defines CardinalInterFilter, I'll make sure that both PRs use similar design choices. I believe it should be possible at some point to conclude that cocardinal filters (cardinality c) are CardinalInterFilters for all cardinalities strictly lower than c.

JADekker avatar Feb 14 '24 17:02 JADekker

I've removed the 'Awaiting-Review' label for now, as I'll first build up the theory of CardinalInterFilters more, these were introduced in #10531. Once this is finished, this PR will also include proofs that cocardinal filters have certain CardinalInterFilter properties.

JADekker avatar Mar 28 '24 17:03 JADekker

This PR has been closed in favour of a newer PR, which makes better use of the recently added CardinalInterFilter file.

JADekker avatar Mar 29 '24 14:03 JADekker