Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-11 16:21 09e08991

View on Github →

fix(analysis/ennreal): fix long-running proofs

Estimated changes

Modified algebra/functions.lean

modified theorem abs_le

modified theorem abs_lt

Modified algebra/linear_algebra/basic.lean

Modified analysis/ennreal.lean

added theorem ennreal.of_real_add

deleted theorem ennreal.of_real_add_of_real

Modified analysis/measure_theory/lebesgue_measure.lean

Modified order/filter.lean

Modified order/zorn.lean

Modified set_theory/ordinal.lean