Theorems · Theorem · order theory

transfiniteIterate_succ

∀ {I : Type u} [inst : SupSet I] (φ : I → I) {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : WellFoundedLT J] (i₀ : I) (j : J),
  ¬IsMax j → transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀)

Defined in

Mathlib.Order.TransfiniteIteration

Cited by

4 results in Mathlib

Foundations

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

Assumes

SupSetLinearOrderSuccOrderWellFoundedLT