Theorems · Inductive type · functional analysis

ContinuousSqrt

(R : Type u_1) → [LE R] → [NonUnitalSemiring R] → [TopologicalSpace R] → Type u_1

A type class encoding the property that there is a continuous square root function on nonnegative elements. This holds for ℝ≥0, ℝ and ℂ (as well as any C⋆-algebra), and this allows us to derive an instance of StarOrderedRing C(α, R) under appropriate hypotheses. In order for this to work on ℝ≥0, we actually must force our square root function to be defined on and well-behaved for pairs x : R × R with x.1 ≤ x.2.

Defined in

Mathlib.Topology.ContinuousMap.StarOrdered

Cited by

43 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

LENonUnitalSemiringTopologicalSpace