Mathlib Map

Theorems · Definition · logic and foundations

ONote.casesOn

{motive : ONote → Sort u} →
  (t : ONote) → motive ONote.zero → ((a : ONote) → (a_1 : ℕ+) → (a_2 : ONote) → motive (a.oadd a_1 a_2)) → motive t
Defined in
Mathlib.SetTheory.Ordinal.Notation
Cited by
3 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ONote.brecOn.eq · cited by 9brecOn.eqONote.ctorIdx · cited by 5ONote.ctorIdxONote.mulNat_eq_mul · cited by 2ONote.mulNat_eq_mulONote.repr_opow · cited by 1ONote.repr_opowONote.ctorElim · cited by 0ONote.ctorElimONote.noConfusion · cited by 0ONote.noConfusionONote.noConfusionType · cited by 0ONote.noConfusionTypePNat · cited by 392PNatONote · cited by 88ONoteONote.casesOnCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • PNatstatement and proof · cited by 392
  • ONotestatement and proof · cited by 88

Cited by7

Results whose statement or proof uses this declaration.