Instances of ContinuousSqrt

This provides the instances of ContinuousSqrt for ℝ, ℝ≥0, and ℂ, thereby yielding instances of StarOrderedRing C(α, R) and StarOrderedRing C(α, R)₀ for any topological space α and R among ℝ≥0, ℝ, and ℂ.

@[instance 100]

noncomputable instance instContinuousSqrtRCLike {𝕜 : Type u_1} [RCLike 𝕜] : ContinuousSqrt 𝕜

Equations

• instContinuousSqrtRCLike = { sqrt := RCLike.ofReal ∘ (fun (x : ℝ) => √x) ∘ ⇑RCLike.re ∘ fun (z : 𝕜 × 𝕜) => z.2 - z.1, continuousOn_sqrt := ⋯, sqrt_nonneg := ⋯, sqrt_mul_sqrt := ⋯ }

noncomputable instance instContinuousSqrtReal : ContinuousSqrt ℝ

Equations

• instContinuousSqrtReal = instContinuousSqrtRCLike

noncomputable instance instContinuousSqrtComplex : ContinuousSqrt ℂ

Equations

• instContinuousSqrtComplex = instContinuousSqrtRCLike

noncomputable instance instContinuousSqrtNNReal : ContinuousSqrt NNReal

Equations

• One or more equations did not get rendered due to their size.