Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-24 10:50 be948000

View on Github →

feat(data/real/nnreal): use the nonneg instance (#9701) ... to show that nnreal forms a conditionally complete linear order with bot. This requires some fixes in the order hierarchy.

  • orders on subtypes are now obtained by lifting coe instead of subtype.val. This has the nice side benefit that some proofs became simpler.
  • subset_conditionally_complete_linear_order is now reducible

Estimated changes

modified theorem nat.subtype.exists_succ