Theorems · Theorem · logic and foundations

Part.fix_def

∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {x : α}
  (h' : ∃ i, (Part.Fix.approx f i x).Dom), Part.fix f x = Part.Fix.approx f (Nat.find h').succ x

Defined in

Mathlib.Control.Fix

Cited by

1 results in Mathlib

Foundations

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