Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.le_of_forall_epsilon_le

Modification history

2021-01-16 03:57
src/data/real/nnreal.lean
chore(data/real/*): rename `le_of_forall_epsilon_le` to `le_of_forall_pos_le_add` (#5761) …
Deleted nnreal.le_of_forall_epsilon_leView on Github →
2020-12-16 07:31
src/data/real/nnreal.lean
chore(*): use notation `ℝ≥0` (#5391)
Modified nnreal.le_of_forall_epsilon_leView on Github →
2020-08-15 20:42
src/data/real/nnreal.lean
fix(*): remove usages of ge/gt (#3808) …
Modified nnreal.le_of_forall_epsilon_leView on Github →
2018-08-21 22:05
data/real/nnreal.lean
refactor(data/real/nnreal): derive order structure for ennreal from with_top nnreal
Added nnreal.le_of_forall_epsilon_leView on Github →