Theorems · Theorem · logic and foundations

OrdinalApprox.gfpApprox_eq_of_mem_fixedPoints

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

The approximations of the greatest fixed point stabilize at a fixed point of f

Defined in: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Cited by: 1 results in Mathlib
Foundations: Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CompleteLattice

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
Ordinalstatement and proof · cited by 1,688
CompleteLatticestatement and proof · cited by 1,048
OrderHomstatement and proof · cited by 934
Function.fixedPointsstatement and proof · cited by 90
OrderHom.dualproof · cited by 48
OrdinalApprox.gfpApproxstatement and proof · cited by 23
OrdinalApprox.lfpApprox_eq_of_mem_fixedPointsproof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

CantorBendixson.perfectKernel_eq_iteratedDerivedSet_of_mem_fixedPointsproof · cited by 1