Commit 2021-08-30 18:18 6adb5e8b
View on Github →feat(topology/algebra/ordered): monotone convergence in pi types (#8841)
- add typeclasses
Sup_convergence_class
andInf_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.