mathlib

6adb5e8b - feat(topology/algebra/ordered): monotone convergence in pi types (#8841)

feat(topology/algebra/ordered): monotone convergence in pi types (#8841) * add typeclasses `Sup_convergence_class` and `Inf_convergence_class` * reformulate theorems about monotone convergence in terms of these typeclasses; * provide instances for a linear order with order topology, for products, and for pi types.