Registry · Proposition I.P45 tau-effective formalized

I.P45 — Monotone Convergence

For tower-compatible monotone function families, the sequence of integrals is non-decreasing across stages.

Book I Part 18 Ch. 84

Dependency Graph

Depends on (2)

I.D99 I.P43

Lean Formalization

Module: TauLib.BookI.Boundary.Integration

Symbol: monotone_convergence_check_step