Theorems · Theorem · logic and foundations

OrdinalApprox.gfpApprox_ord_mem_fixedPoint

∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  f x ≤ x → OrdinalApprox.gfpApprox f x (Order.succ (Cardinal.mk α)).ord ∈ Function.fixedPoints ⇑f

The approximation at the index of the successor of the domain's cardinality is a fixed point

Defined in

Mathlib.SetTheory.Ordinal.FixedPointApproximants

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLattice