BoundedContinuous

📁 Source: Mathlib/Analysis/RCLike/BoundedContinuous.lean

Statistics

Metric	Count
Definitions	0
Theorems restrict_toContinuousMap_eq_toContinuousMapStar_restrict	1
Total	1

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrict_toContinuousMap_eq_toContinuousMapStar_restrict 📖	mathematical	—	Subalgebra.map Real BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedCommRing.toNormedRing Real.normedCommRing ContinuousMap PseudoMetricSpace.toUniformSpace Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField BoundedContinuousFunction.instSemiring Ring.toSemiring NormedRing.toRing instBoundedMul NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing IsTopologicalSemiring.toContinuousMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing instBoundedAddOfLipschitzAdd ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedAddCommGroup.to_lipschitzAdd NonUnitalSeminormedRing.toSeminormedAddCommGroup IsTopologicalSemiring.toContinuousAdd BoundedContinuousFunction.instAlgebra toNormedAlgebra Real.instRCLike ContinuousMap.instSemiringOfIsTopologicalSemiring ContinuousMap.algebra NormedAlgebra.toAlgebra BoundedContinuousFunction.toContinuousMapₐ Subalgebra.comap NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField BoundedContinuousFunction.AlgHom.compLeftContinuousBounded ofRealAm NNReal instOneNNReal lipschitzWith_ofReal Subalgebra.restrictScalars SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing NonUnitalNormedCommRing.toNonUnitalNormedRing NormedAlgebra.id BoundedContinuousFunction.instIsScalarTower MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Algebra.toSMul SeminormedRing.toRing CommSemiring.toSemiring IsScalarTower.right StarSubalgebra.toSubalgebra toStarRing BoundedContinuousFunction.instStarRing CStarRing.to_normedStarGroup instCStarRing BoundedContinuousFunction.instStarModule StarRing.toStarAddMonoid NormedField.toNormedSpace StarMul.toStarModule CommRing.toCommMonoid Field.toCommRing StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CommRing.toRing Real.pseudoMetricSpace Real.semiring instIsTopologicalRingReal Algebra.id AlgHom.compLeftContinuous continuous_ofReal ContinuousMap.instIsScalarTower ContinuousMap.instStarRingOfContinuousStar instContinuousStar ContinuousMap.instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarSubalgebra.map BoundedContinuousFunction.toContinuousMapStarₐ	—	instBoundedMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalSemiring.toContinuousAdd CStarRing.to_normedStarGroup instCStarRing BoundedContinuousFunction.instStarModule StarMul.toStarModule Subalgebra.ext NonUnitalSeminormedRing.toIsTopologicalRing lipschitzWith_ofReal BoundedContinuousFunction.instIsScalarTower IsScalarTower.right instIsTopologicalRingReal continuous_ofReal ContinuousMap.instIsScalarTower instContinuousStar ContinuousMap.instStarModule ContinuousMap.ext instFaithfulSMul_1 DivisionRing.isSimpleRing IsSimpleRing.instNontrivial DFunLike.congr_fun RingHomIsometric.ids ContinuousLinearMap.lipschitz BoundedContinuousFunction.ext ofReal_re

---

← Back to Index