Mathlib v3 is deprecated. Go to Mathlib v4

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 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.

Estimated changes

modified theorem tendsto_at_bot_cinfi
modified theorem tendsto_at_bot_csupr
modified theorem tendsto_at_bot_infi
modified theorem tendsto_at_bot_is_glb
added theorem tendsto_at_bot_is_lub
modified theorem tendsto_at_bot_supr
modified theorem tendsto_at_top_cinfi
modified theorem tendsto_at_top_csupr
modified theorem tendsto_at_top_infi
added theorem tendsto_at_top_is_glb
modified theorem tendsto_at_top_is_lub
modified theorem tendsto_at_top_supr