Documentation

Mathlib.Topology.ContinuousFunction.StarOrdered

Continuous functions as a star-ordered ring #

theorem ContinuousMap.starOrderedRing_of_sqrt {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [TopologicalSpace R] [ContinuousStar R] [TopologicalRing R] (sqrt : RR) (h_continuousOn : ContinuousOn sqrt {x : R | 0 x}) (h_sqrt : ∀ (x : R), 0 xstar (sqrt x) * sqrt x = x) :
@[instance 100]
instance ContinuousMap.instStarOrderedRingRCLike {α : Type u_1} [TopologicalSpace α] {𝕜 : Type u_2} [RCLike 𝕜] :
Equations
  • =