Mathlib Map

Theorems · Definition · logic and foundations

ONote.below

{motive : ONote → Sort u} → ONote → Sort (max 1 u)
Defined in
Mathlib.SetTheory.Ordinal.Notation
Cited by
10 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 · cited by 12ONote.brecOnONote.brecOn.go · cited by 10brecOn.goONote.brecOn.eq · cited by 9brecOn.eqONote.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.belowCITED BYCITES

Cites2

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

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

Cited by12

Results whose statement or proof uses this declaration.