Mathlib Map

Theorems · Definition · logic and foundations

NONote.mk

(o : ONote) → [h : o.NF] → NONote

Construct a NONote from an ordinal notation (and infer normality)

Defined in
Mathlib.SetTheory.Ordinal.Notation
Cited by
0 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
ONote.NF
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NONote.opow · cited by 1NONote.opowONote · cited by 88ONoteONote.NF · cited by 36ONote.NFNONote · cited by 6NONoteNONote.mkCITED BYCITES

Cites3

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

  • ONotestatement and proof · cited by 88
  • ONote.NFstatement and proof · cited by 36
  • NONotestatement · cited by 6

Cited by1

Results whose statement or proof uses this declaration.