Theorems · Definition · logic and foundations

NONote.recOn

{C : NONote → Sort u_1} →
  (o : NONote) → C 0 → ((e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)) → C o

This is a recursor-like theorem for NONote suggesting an inductive definition, which can't actually be defined this way due to conflicting dependencies.

Defined in

Mathlib.SetTheory.Ordinal.Notation

Cited by

0 results in Mathlib

Foundations

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