Mathlib Map

Theorems · Theorem · logic and foundations

ONote.brecOn.eq

∀ {motive : ONote → Sort u} (t : ONote) (F_1 : (t : ONote) → ONote.below t → motive t),
  ONote.brecOn t F_1 = F_1 t (ONote.brecOn.go t F_1).2
Defined in
Mathlib.SetTheory.Ordinal.Notation
Cited by
9 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ONote.repr.eq_def · cited by 1repr.eq_defONote.scale.eq_def · cited by 0scale.eq_defONote.fundamentalSequence.eq_def · cited by 0fundamentalSequence.eq_defONote.cmp.eq_def · cited by 0cmp.eq_defONote.split.eq_def · cited by 0split.eq_defONote.split'.eq_def · cited by 0split'.eq_defONote.mul.eq_def · cited by 0mul.eq_defONote.sub.eq_def · cited by 0sub.eq_defONote.add.eq_def · cited by 0add.eq_defPNat · cited by 392PNatONote · cited by 88ONoteONote.brecOn · cited by 12ONote.brecOnONote.brecOn.go · cited by 10brecOn.goONote.below · cited by 10ONote.belowONote.casesOn · cited by 3ONote.casesOnbrecOn.eqCITED BYCITES

Cites6

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

Cited by9

Results whose statement or proof uses this declaration.