TopDualPairing

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

Statistics

Metric	Count
Definitions	0
Theorems topDualPairing_isContPerfPair	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topDualPairing_isContPerfPair 📖	mathematical	—	LinearMap.IsContPerfPair ContinuousLinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule EuclideanDomain.toCommRing Field.toEuclideanDomain ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing IsSemitopologicalSemiring.toContinuousAdd ContinuousLinearMap.topologicalSpace topDualPairing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsSemitopologicalSemiring.toContinuousAdd IsModuleTopology.continuous_bilinear_of_finite_left isModuleTopologyOfFiniteDimensional ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids RingHomIsometric.ids IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring ContinuousLinearMap.instT2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousLinearMap.instModuleFinite IsSimpleModule.instIsNoetherian instIsSimpleModule Function.bijective_id Function.Bijective.comp RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul SMulCommClass.symm LinearEquiv.bijective LinearMap.flip_bijective_iff₁

---

← Back to Index