Theorems · Theorem · logic and foundations

OrdinalApprox.lfpApprox_eq_of_mem_fixedPoints

∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}},
  a ≤ b →
    OrdinalApprox.lfpApprox f x a ∈ Function.fixedPoints ⇑f →
      OrdinalApprox.lfpApprox f x b = OrdinalApprox.lfpApprox f x a

The approximations of the least fixed point stabilize at a fixed point of f

Defined in

Mathlib.SetTheory.Ordinal.FixedPointApproximants

Cited by

4 results in Mathlib

Foundations

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

Assumes

CompleteLattice