Basic

📁 Source: Mathlib/Analysis/Normed/Algebra/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems instCompactSpaceElemCharacterSpaceOfProperSpace, norm_le_norm_one	2
Total	2

WeakDual.CharacterSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompactSpaceElemCharacterSpaceOfProperSpace 📖	mathematical	—	CompactSpace Set.Elem WeakDual Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Algebra.id Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing WeakDual.characterSpace instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceWeakDual	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul isCompact_iff_compactSpace RingHomInvPair.ids Algebra.to_smulCommClass RingHomIsometric.ids Set.mem_preimage mem_closedBall_zero_iff norm_le_norm_one IsCompact.of_isClosed_subset WeakDual.isCompact_closedBall isClosed NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsLocalRing.toNontrivial Field.instIsLocalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
norm_le_norm_one 📖	mathematical	—	Real Real.instLE Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedRing.toSeminormedRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace ContinuousLinearMap.hasOpNorm NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids WeakDual Semifield.toCommSemiring IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Algebra.id Ring.uniformContinuousConstSMul NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul instAddCommMonoidWeakDual ContinuousLinearMap.addCommMonoid Semiring.toModule WeakDual.instModule' Algebra.to_smulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ContinuousLinearMap.module AddCommMonoid.toAddMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv WeakDual.toStrongDual Set Set.instMembership WeakDual.characterSpace NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.opNorm_le_bound RingHomInvPair.ids Algebra.to_smulCommClass norm_nonneg spectrum.norm_le_norm_mul_of_mem apply_mem_spectrum NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsLocalRing.toNontrivial Field.instIsLocalRing mul_comm

---

← Back to Index