Part.Fix.approx_mono'

theorem Part.Fix.approx_mono' : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {i : ℕ}, Part.Fix.approx (⇑f) i ≤ Part.Fix.approx (⇑f) i.succ

The theorem `Part.Fix.approx_mono'` states that for any type `α`, any type function `β` mapping `α` to another type, and any function `f` that is a monotone function from partial functions from `α` to `β` to another such partial function, then for any natural number `i`, the `i`-th step in the approximation chain of the fixed point of `f` is less than or equal to the `(i+1)`-th step in the approximation chain. In other words, the series of approximations to the fixed point of `f` is non-decreasing.

More concisely: For any monotone function `f` from partial functions on a type `α` to partial functions on another type `β`, the approximation chain of `f`'s fixed point is non-decreasing.