feat: Tendsto (√·) atTop atTop (#33837)

From [CLT](https://github.com/RemyDegenne/CLT/blob/07a49e97b1c745d306d301200a97c48eeb299205/Clt/CLT.lean#L34).
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 (√·)`.

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

Mathlib/Data/Real/Sqrt.lean

@@ -119,12 +119,24 @@ variable {x y : ℝ}
 theorem coe_sqrt {x : ℝ≥0} : (NNReal.sqrt x : ℝ) = √(x : ℝ) := by
   rw [Real.sqrt, Real.toNNReal_coe]
 
-@[continuity]
-theorem continuous_sqrt : Continuous (√· : ℝ → ℝ) := by
+@[continuity, fun_prop]
+theorem continuous_sqrt : Continuous (√· : ℝ → ℝ) := by unfold sqrt; fun_prop
+
+@[simp]
+lemma map_sqrt_atTop : map (√·) atTop = atTop := by
   unfold sqrt
-  exact NNReal.continuous_coe.comp <| NNReal.continuous_sqrt.comp continuous_real_toNNReal
+  change map (NNReal.toReal ∘ NNReal.sqrt ∘ Real.toNNReal) atTop = atTop
+  simp [← map_map]
+
+@[simp]
+lemma comap_sqrt_atTop : comap (√·) atTop = atTop := by
+  unfold sqrt
+  change comap (NNReal.toReal ∘ NNReal.sqrt ∘ Real.toNNReal) atTop = atTop
+  simp [← comap_comap]
+
+lemma tendsto_sqrt_atTop : Tendsto (√·) atTop atTop := map_sqrt_atTop.le
 
-theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0 := by simp [sqrt, Real.toNNReal_eq_zero.2 h]
+theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : √x = 0 := by simp [sqrt, Real.toNNReal_eq_zero.2 h]
 
 @[simp] theorem sqrt_nonneg (x : ℝ) : 0 ≤ √x := by
   unfold sqrt