Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.le_of_forall_pos_le_add

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) …

Added nnreal.le_of_forall_pos_le_add View on Github →