Theorems · Theorem · logic and foundations

OrdinalApprox.lfpApprox_le_of_mem_fixedPoints

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

Every value of the approximation is less or equal than every fixed point of f greater or equal than the initial value

Defined in

Mathlib.SetTheory.Ordinal.FixedPointApproximants

Cited by

3 results in Mathlib

Foundations

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

Assumes

CompleteLattice