Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-24 05:29 c6a7f300

View on Github →

refactor(set_theory/ordinal): shorten proof of well_ordering_thm (#1078)

  • refactor(set_theory/ordinal): shorten proof of well_ordering_thm§
  • Update ordinal.lean
  • Update ordinal.lean
  • Update ordinal.lean
  • Improve readability
  • shorten proof
  • Shorten proof

Estimated changes