Theorems · Theorem · logic and foundations

Partrec.fix_aux

∀ {α : Type u_5} {σ : Type u_6} (f : α →. σ ⊕ α) (a : α) (b : σ),
  have F := fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n;
  (∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ f.fix a

Defined in

Mathlib.Computability.Partrec

Cited by

1 results in Mathlib

Foundations

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