Theorems · Theorem · logic and foundations

OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq

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

If the sequence of ordinal-indexed approximations takes a value twice, then it actually stabilised at that value.

Defined in

Mathlib.SetTheory.Ordinal.FixedPointApproximants

Cited by

3 results in Mathlib

Foundations

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

Assumes

CompleteLattice