Commit 2023-02-06 08:48 23bcb179

View on Github →

feat: port/Topology.Algebra.Order.MonotoneConvergence (#2097) port of topology.algebra.order.monotone_convergence

Estimated changes

added theorem Antitone.ge_of_tendsto
added theorem Antitone.le_of_tendsto
added theorem Monotone.ge_of_tendsto
added theorem Monotone.le_of_tendsto
added theorem infᵢ_eq_of_tendsto
added theorem isGLB_of_tendsto_atBot
added theorem isGLB_of_tendsto_atTop
added theorem isLUB_of_tendsto_atBot
added theorem isLUB_of_tendsto_atTop
added theorem supᵢ_eq_of_tendsto
added theorem tendsto_atBot_cinfi
added theorem tendsto_atBot_csupr
added theorem tendsto_atBot_infᵢ
added theorem tendsto_atBot_isGLB
added theorem tendsto_atBot_isLUB
added theorem tendsto_atBot_supᵢ
added theorem tendsto_atTop_cinfi
added theorem tendsto_atTop_csupr
added theorem tendsto_atTop_infᵢ
added theorem tendsto_atTop_isGLB
added theorem tendsto_atTop_isLUB
added theorem tendsto_atTop_supᵢ
added theorem tendsto_of_monotone