LinearIsometry

📁 Source: Mathlib/Analysis/Convex/LinearIsometry.lean

Statistics

Metric	Count
Definitions	0
Theorems strictConvexSpace, strictConvexSpace_range, strictConvexSpace_range_iff, strictConvexSpace_iff, strictConvex_image, strictConvex_preimage, linearIsometry_preimage, instStrictConvexSpace	8
Total	8

LinearIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvexSpace 📖	mathematical	—	StrictConvexSpace	—	Isometry.preimage_closedBall isometry StrictConvex.linearIsometry_preimage strictConvex_closedBall
strictConvexSpace_range 📖	mathematical	—	StrictConvexSpace Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids SemilinearMapClass.semilinearMap LinearIsometry instFunLike SemilinearIsometryClass.toSemilinearMapClass instSemilinearIsometryClass Submodule.normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.normedSpace Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	RingHomSurjective.ids SemilinearIsometryClass.toSemilinearMapClass instSemilinearIsometryClass IsScalarTower.left strictConvexSpace_range_iff
strictConvexSpace_range_iff 📖	mathematical	—	StrictConvexSpace Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids SemilinearMapClass.semilinearMap LinearIsometry instFunLike SemilinearIsometryClass.toSemilinearMapClass instSemilinearIsometryClass Submodule.normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.normedSpace Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	RingHomSurjective.invPair RingHomInvPair.ids IsScalarTower.left LinearIsometryEquiv.strictConvexSpace_iff

LinearIsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvexSpace_iff 📖	mathematical	—	StrictConvexSpace	—	RingHomInvPair.ids map_zero image_closedBall strictConvex_image
strictConvex_image 📖	mathematical	—	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toModule Set.image DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike	—	RingHomInvPair.ids ContinuousLinearEquiv.strictConvex_image
strictConvex_preimage 📖	mathematical	—	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toModule Set.preimage DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike	—	RingHomInvPair.ids ContinuousLinearEquiv.strictConvex_preimage

StrictConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearIsometry_preimage 📖	mathematical	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toModule	NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid Set.preimage DFunLike.coe LinearIsometry RingHom.id Semiring.toNonAssocSemiring LinearIsometry.instFunLike	—	linear_preimage LinearIsometry.continuous LinearIsometry.injective

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStrictConvexSpace 📖	mathematical	—	StrictConvexSpace Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership setLike normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing normedSpace Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	LinearIsometry.strictConvexSpace IsScalarTower.left

---

← Back to Index