Documentation
Mathlib
.
Topology
.
Algebra
.
Star
.
Real
Search
return to top
source
Imports
Init
Mathlib.Basic.NNReal.Star
Mathlib.Topology.Algebra.Star
Mathlib.Topology.MetricSpace.Pseudo.Constructions
Imported by
instContinuousStarReal
NNReal
.
instContinuousStar
← Mathematical handbook
Topological properties of conjugation on ℝ
#
source
instance
instContinuousStarReal
:
ContinuousStar
ℝ
source
instance
NNReal
.
instContinuousStar
:
ContinuousStar
NNReal