Defining CardinalInterFilter to extend CountableInterFilter

Stream: mathlib4

[Josha Dekker]

Hi all, I'm trying to define CardinalInterFilter as a generalisation of CountableInterFilter. I have made PR #10531 for this purpose, in which I try to define this concept and show that it corresponds to the CountableInterFilter for a suitable choice of cardinality. I'd much recommend any feedback! I think that I can generalise most of the API from CountableInterFilter, but I'm keeping this PR a bit small until we have agreement that the way that I set up CardinalInterFilter is desirable.

In particular, I would like to hear your thoughts on:

1. ordering of the arguments in CardinalInterFilter: should I start with the filter and then the cardinality, or vice versa? the latter seems closer to the naming of the object, but the former stresses more that this is a property for filters.
2. should I aim to redefine CountableInterFilter purely in terms of CardinalInterFilter?

Motivation for introducing CardinalInterFilter: this would be the way to go to introduce K-Lindelöf spaces, where the condition would be exactly in terms of these CardinalInterFilters:

def IsCardinalLindelof (s : Set X) (c : Cardinal.{u}):=
  ∀ ⦃f⦄ [NeBot f] [CardinalInterFilter f c], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f

It is clear that for c = aleph0, this reduces to IsCompact, whereas for c = aleph1, this reduces to IsLindelof.