PerfectPairing

📁 Source: Mathlib/Topology/Algebra/Module/PerfectPairing.lean

Statistics

Metric	Count
Definitions IsContPerfPair, toContPerfPair	2
Theorems bijective_left, bijective_right, continuous_uncurry, ext, ext_iff, continuous_of_isContPerfPair, continuous_uncurry_of_isContPerfPair, instIsContPerfPair, toContPerfPair_apply, toLinearMap_toContPerfPair	10
Total	12

LinearMap

Definitions

Name	Category	Theorems
IsContPerfPair 📖	CompData	2 math math: InnerProductSpace.instIsContPerfPairRealInnerₗOfCompleteSpace, flip.instIsContPerfPair
toContPerfPair 📖	CompOp	3 math math: toLinearMap_toContPerfPair, ProperCone.dual_singleton, toContPerfPair_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_of_isContPerfPair 📖	mathematical	—	Continuous DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass Continuous.comp continuous_uncurry_of_isContPerfPair Continuous.prodMk_right
continuous_uncurry_of_isContPerfPair 📖	mathematical	—	Continuous instTopologicalSpaceProd DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id	—	IsContPerfPair.continuous_uncurry
toContPerfPair_apply 📖	mathematical	—	DFunLike.coe StrongDual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearEquiv RingHomInvPair.ids ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring EquivLike.toFunLike LinearEquiv.instEquivLike toContPerfPair LinearMap instFunLike addCommMonoid module	—	Algebra.to_smulCommClass RingHomInvPair.ids IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul
toLinearMap_toContPerfPair 📖	mathematical	—	ContinuousLinearMap.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule DFunLike.coe LinearEquiv RingHomInvPair.ids StrongDual ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring EquivLike.toFunLike LinearEquiv.instEquivLike toContPerfPair LinearMap addCommMonoid module instFunLike	—	Algebra.to_smulCommClass RingHomInvPair.ids IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul

LinearMap.IsContPerfPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_left 📖	mathematical	—	Function.Bijective ContinuousLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instFunLike Continuous.comp instTopologicalSpaceProd continuous_uncurry Continuous.prodMk_right	—	Algebra.to_smulCommClass
bijective_right 📖	mathematical	—	Function.Bijective ContinuousLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id LinearMap.instFunLike LinearMap.flip Continuous.comp instTopologicalSpaceProd continuous_uncurry Continuous.prodMk_left	—	Algebra.to_smulCommClass
continuous_uncurry 📖	mathematical	—	Continuous instTopologicalSpaceProd DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass
ext 📖	—	—	—	—	Algebra.to_smulCommClass Continuous.comp Continuous.prodMk_right SMulCommClass.symm Continuous.prodMk_left
ext_iff 📖	—	—	—	—	Algebra.to_smulCommClass ext

LinearMap.flip

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsContPerfPair 📖	mathematical	—	LinearMap.IsContPerfPair LinearMap.flip CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass Continuous.comp LinearMap.continuous_uncurry_of_isContPerfPair continuous_swap LinearMap.IsContPerfPair.bijective_right LinearMap.IsContPerfPair.bijective_left

---

← Back to Index