Theorems · Theorem · logic and foundations

OrdinalApprox.gfpApprox_mem_fixedPoints_of_eq

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

Defined in: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Cited by: 0 results in Mathlib
Foundations: Depth 46 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 · cited by 90
OrderHom.dualproof · cited by 48
OrdinalApprox.gfpApproxstatement and proof · cited by 23
OrdinalApprox.lfpApprox_mem_fixedPoints_of_eqproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.