Commit 2026-01-11 19:44 622f41ab

View on Github →

feat: Tendsto (√·) atTop atTop (#33837) From CLT. I proved the more strong statements: map (√·) atTop = atTop and comap (√·) atTop = atTop. While I'm at it, I added a fun_prop attr to Continuous (√·).

Estimated changes

added theorem Real.comap_sqrt_atTop
modified theorem Real.continuous_sqrt
added theorem Real.map_sqrt_atTop
modified theorem Real.sqrt_eq_zero_of_nonpos