Documentation

Mathlib.Topology.ContinuousMap.ContinuousSqrt

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 ℂ.

source
@[instance 100]
noncomputable instance instContinuousSqrtRCLike {𝕜 : Type u_1} [RCLike 𝕜] :
ContinuousSqrt 𝕜
Equations
    source
    noncomputable instance instContinuousSqrtReal :
    ContinuousSqrt ℝ
    Equations
      source
      noncomputable instance instContinuousSqrtComplex :
      ContinuousSqrt ℂ
      Equations
        source
        noncomputable instance instContinuousSqrtNNReal :
        ContinuousSqrt NNReal
        Equations