Theorems · Theorem · logic and foundations

ONote.fundamentalSequence.eq_def

∀ (x : ONote),
  x.fundamentalSequence =
    match x with
    | ONote.zero => Sum.inl none
    | a.oadd m b =>
      match b.fundamentalSequence with
      | Sum.inr f => Sum.inr fun i => a.oadd m (f i)
      | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
      | Sum.inl none =>
        match a.fundamentalSequence, m.natPred with
        | Sum.inl none, 0 => Sum.inl (some ONote.zero)
        | Sum.inl none, m.succ => Sum.inl (some (ONote.zero.oadd m.succPNat ONote.zero))
        | Sum.inl (some a'), 0 => Sum.inr fun i => a'.oadd i.succPNat ONote.zero
        | Sum.inl (some a'), m.succ => Sum.inr fun i => a.oadd m.succPNat (a'.oadd i.succPNat ONote.zero)
        | Sum.inr f, 0 => Sum.inr fun i => (f i).oadd 1 ONote.zero
        | Sum.inr f, m.succ => Sum.inr fun i => a.oadd m.succPNat ((f i).oadd 1 ONote.zero)

Defined in

Mathlib.SetTheory.Ordinal.Notation

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext