Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.le_of_forall_epsilon_le

Modification history

2021-01-16 03:57
src/data/real/basic.lean
chore(data/real/*): rename `le_of_forall_epsilon_le` to `le_of_forall_pos_le_add` (#5761) …
Deleted real.le_of_forall_epsilon_leView on Github →
2020-08-15 20:42
src/data/real/basic.lean
fix(*): remove usages of ge/gt (#3808) …
Modified real.le_of_forall_epsilon_leView on Github →
2018-11-05 09:39
data/real/basic.lean
feat(analysis/metric_spaces): Compact and proper spaces (#430)
Added real.le_of_forall_epsilon_leView on Github →