Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-06 22:46 bb1fb897

View on Github →

feat(data/real/basic): add real.Inf_le_iff (#7524) From LTE.

Estimated changes

Modified src/algebra/ordered_group.lean

added theorem le_iff_forall_pos_le_add

added theorem le_iff_forall_pos_lt_add

Modified src/data/real/basic.lean

added theorem real.Inf_le_iff

added theorem real.add_pos_lt_Sup

added theorem real.le_Sup_iff

added theorem real.lt_Inf_add_pos