Theorems · Definition · logic and foundations

Part.fix

{α : Type u_1} → {β : α → Type u_2} → (((a : α) → Part (β a)) → (a : α) → Part (β a)) → (x : α) → Part (β x)

The least fixed point of f. If f is a continuous function (according to complete partial orders), it satisfies the equations: 1. fix f = f (fix f) (is a fixed point) 2. ∀ X, f X ≤ X → fix f ≤ X (least fixed point)

Defined in

Mathlib.Control.Fix

Cited by

9 results in Mathlib

Foundations

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