Theorems · Definition · logic and foundations

PFun.fixInduction

{α : Type u_1} →
  {β : Type u_2} →
    {C : α → Sort u_7} →
      {f : α →. β ⊕ α} →
        {b : β} →
          {a : α} → b ∈ f.fix a → ((a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a') → C a

A recursion principle for PFun.fix.

Defined in

Mathlib.Data.PFun

Cited by

6 results in Mathlib

Foundations

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