Theorems · Theorem · logic and foundations

PFun.fixInduction_spec

∀ {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
  (H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'),
  PFun.fixInduction h H = H a h fun x h' => PFun.fixInduction ⋯ H

Defined in

Mathlib.Data.PFun

Cited by

2 results in Mathlib

Foundations

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