Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.continuous_sqrt

Modification history

2020-12-16 13:55

src/data/real/sqrt.lean

refactor(data/real): move `real.sqrt` to `data.real.sqrt`, more dependencies (#5359) …

Added nnreal.continuous_sqrt View on Github →