Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-05 22:52 e4b652f6

View on Github →

refactor(data/real/basic): rename for consistency

Estimated changes

Modified analysis/real.lean

deleted theorem exists_supremum_real

Modified data/real/basic.lean

deleted theorem real.Sup_is_lub

Modified data/real/ennreal.lean