Theorems · Theorem · logic and foundations

OrdinalApprox.iSup_lfpApprox_eq_of_mem_fixedPoints

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

If lfpApprox f x a is a fixed point, then the supremum of the whole ordinal-indexed sequence equals the value at a.

Defined in

Mathlib.SetTheory.Ordinal.FixedPointApproximants

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteLattice