Theorems · Definition · order theory

Part.Fix.approxChain

{α : Type u_1} →
  {β : α → Type u_2} →
    (((a : α) → Part (β a)) →o (a : α) → Part (β a)) → OmegaCompletePartialOrder.Chain ((a : α) → Part (β a))

The series of approximations of fix f (see approx) as a Chain

Defined in

Mathlib.Control.LawfulFix

Cited by

6 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound