Theorems · Theorem · order theory

transfiniteIterate.congr_simp

∀ {I : Type u} [inst : SupSet I] (φ φ_1 : I → I),
  φ = φ_1 →
    ∀ {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : WellFoundedLT J] (j j_1 : J),
      j = j_1 → ∀ (a a_1 : I), a = a_1 → transfiniteIterate φ j a = transfiniteIterate φ_1 j_1 a_1

Defined in

Mathlib.Order.TransfiniteIteration

Cited by

0 results in Mathlib

Foundations

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

Assumes

SupSetLinearOrderSuccOrderWellFoundedLT