Theorems · Theorem · order theory

monotone_transfiniteIterate

∀ {I : Type u} [inst : CompleteLattice I] (φ : I → I) (i₀ : I) {J : Type w} [inst_1 : LinearOrder J] [OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J], (∀ (i : I), i ≤ φ i) → Monotone fun j => transfiniteIterate φ j i₀

Defined in

Mathlib.Order.TransfiniteIteration

Cited by

3 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLatticeLinearOrderOrderBotSuccOrderWellFoundedLT