Mathlib Map

Theorems · Definition · logic and foundations

ONote.NFBelow.casesOn

∀ {motive : (a : ONote) → (a_1 : Ordinal.{0}) → a.NFBelow a_1 → Prop} {a : ONote} {a_1 : Ordinal.{0}}
  (t : a.NFBelow a_1),
  (∀ {b : Ordinal.{0}}, motive 0 b ⋯) →
    (∀ {e : ONote} {n : ℕ+} {a : ONote} {eb b : Ordinal.{0}} (a_2 : e.NFBelow eb) (a_3 : a.NFBelow e.repr)
        (a_4 : e.repr < b), motive (e.oadd n a) b ⋯) →
      motive a a_1 t
Defined in
Mathlib.SetTheory.Ordinal.Notation
Cited by
4 results in Mathlib
Foundations
Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ONote.NF.below_of_lt · cited by 6NF.below_of_ltONote.NFBelow.lt · cited by 2NFBelow.ltONote.NFBelow.snd · cited by 1NFBelow.sndONote.NFBelow.fst · cited by 1NFBelow.fstOrdinal · cited by 1688OrdinalPNat · cited by 392PNatONote · cited by 88ONoteONote.repr · cited by 45ONote.reprONote.NFBelow · cited by 20ONote.NFBelowNFBelow.casesOnCITED BYCITES

Cites5

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

  • Ordinalstatement and proof · cited by 1,688
  • PNatstatement and proof · cited by 392
  • ONotestatement and proof · cited by 88
  • ONote.reprstatement and proof · cited by 45
  • ONote.NFBelowstatement and proof · cited by 20

Cited by4

Results whose statement or proof uses this declaration.