Find home for lemmas about indicators and cardinality

Stream: lean4

[Damien Thomine]

From PR19039: there are a few lemmas about cardinality/sum of indicators/limits we would like to put in a new file to simplify some imports.

The questions are: under what name, and where?

These lemmas use, among others:

• Algebra.Order.Group.Indicator
• Order.Filter.AtTopBot.Archimedean
• Topology.Algebra.Order.LiminfLimsup

They are used in:

• Probability.Martingale.BorelCantelli

I have no real idea for both. Location might be somewhat logical somewhere in Topology.Algebra?

[Kim Morrison]

Yes, Topology.Algebra is pretty clearly the latest of the "top-level" directories used there, so that's a natural place to start.