Theorems · Theorem · logic and foundations

OrdinalApprox.exists_lfpApprox_eq_lfpApprox

∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : α),
  ∃ a < (Order.succ (Cardinal.mk α)).ord,
    ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ OrdinalApprox.lfpApprox f x a = OrdinalApprox.lfpApprox f x b

There are distinct indices smaller than the successor of the domain's cardinality yielding the same value

Defined in

Mathlib.SetTheory.Ordinal.FixedPointApproximants

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteLattice