StarOrdered

📁 Source: Mathlib/Topology/ContinuousMap/StarOrdered.lean

Statistics

Metric	Count
Definitions	0
Theorems instStarOrderedRingOfContinuousSqrt, instStarOrderedRing, continuousOn_sqrt, sqrt_mul_sqrt, sqrt_nonneg	5
Total	5

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarOrderedRingOfContinuousSqrt 📖	mathematical	—	StarOrderedRing ContinuousMap instNonUnitalSemiringOfIsTopologicalSemiring partialOrder instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	StarOrderedRing.of_le_iff le_def ContinuousOn.restrict ContinuousSqrt.continuousOn_sqrt Continuous.codRestrict ContinuousMapClass.map_continuous instContinuousMapClass ext IsSelfAdjoint.star_eq IsSelfAdjoint.of_nonneg ContinuousSqrt.sqrt_nonneg ContinuousSqrt.sqrt_mul_sqrt le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono StarOrderedRing.toIsOrderedAddMonoid star_mul_self_nonneg

ContinuousMapZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarOrderedRing 📖	mathematical	—	StarOrderedRing ContinuousMapZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalCommSemiring.toNonUnitalSemiring instNonUnitalCommSemiring instPartialOrder instStarRing	—	le_def instContinuousMapClass ContinuousMap.coe_coe ContinuousMap.le_def StarOrderedRing.le_iff AddSubmonoid.closure_induction_left ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubmonoid.instAddSubmonoidClass ext IsTopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toContinuousMul map_zero instZeroHomClass zero_add StarOrderedRing.nonneg_iff le_antisymm LE.le.trans_eq le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono StarOrderedRing.toIsOrderedAddMonoid star_mul_self_nonneg add_assoc AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubmonoid.subset_closure AddSubmonoid.closure_induction add_zero

ContinuousSqrt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_sqrt 📖	mathematical	—	ContinuousOn instTopologicalSpaceProd sqrt setOf	—	—
sqrt_mul_sqrt 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring Distrib.toMul sqrt	—	—
sqrt_nonneg 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalSemiring.toNonUnitalNonAssocSemiring sqrt	—	—

---

← Back to Index