HahnBanach

📁 Source: Mathlib/Analysis/Normed/Module/HahnBanach.lean

Statistics

Metric	Count
Definitions	0
Theorems exist_extension_of_finiteDimensional_range, exists_extension_norm_eq, of_finiteDimensional, exists_dual_vector, exists_dual_vector', exists_dual_vector'', exists_extension_norm_eq	7
Total	7

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exist_extension_of_finiteDimensional_range 📖	mathematical	—	comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SetLike.instMembership Submodule.setLike instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Submodule.addCommMonoid NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.module RingHomCompTriple.ids Submodule.subtypeL	—	RingHomSurjective.ids commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing RingHomInvPair.ids Submodule.topologicalAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SMulMemClass.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Submodule.smulMemClass RCLike.toCompleteSpace Finite.of_fintype instT2SpaceSubtype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace RingHomCompTriple.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing LinearMap.mem_range_self IsScalarTower.left ext Module.Basis.equivFunL_symm_apply_repr exists_extension_norm_eq

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_extension_norm_eq 📖	mathematical	—	DFunLike.coe StrongDual Real semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule normedField ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Subspace instDivisionRing SetLike.instMembership Submodule.setLike DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module Norm.norm ContinuousLinearMap.hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing DenselyNormedField.toNontriviallyNormedField denselyNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField Submodule.seminormedAddCommGroup instRing Submodule.normedSpace Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.left instMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left exists_extension_of_le_sublinear norm_smul NormedSpace.toNormSMulClass abs_of_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_left_comm left_distrib Distrib.leftDistribClass mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono instIsOrderedRing norm_add_le norm_nonneg RingHomIsometric.ids le_trans le_abs_self ContinuousLinearMap.le_opNorm abs_le neg_le covariant_swap_add_of_covariant_add norm_neg LinearMap.map_neg le_antisymm LinearMap.mkContinuous_norm_le ContinuousLinearMap.opNorm_le_bound

Submodule.ClosedComplemented

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_finiteDimensional 📖	mathematical	—	Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	IsScalarTower.left RingHomCompTriple.ids ContinuousLinearMap.exist_extension_of_finiteDimensional_range LinearMap.finiteDimensional_range DFunLike.congr_fun

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_dual_vector 📖	mathematical	—	Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing DenselyNormedField.toNontriviallyNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Real Real.instOne DFunLike.coe ContinuousLinearMap.funLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RCLike.ofReal SeminormedAddCommGroup.toNorm	—	RingHomInvPair.ids DivisionRing.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors ne_zero_of_norm_ne_zero LinearEquiv.toSpanNonzeroSingleton_homothety NormedSpace.toNormSMulClass lt_of_le_of_ne' norm_nonneg Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsScalarTower.left exists_extension_norm_eq instIsRCLikeNormedField Submodule.mem_span_singleton_self LinearEquiv.coord_self instIsDomain mul_one le_antisymm norm_smul RingHomIsometric.ids norm_algebraMap' NormedDivisionRing.to_normOneClass norm_norm le_imp_le_of_le_of_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing ContinuousLinearMap.opNorm_le_bound le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Eq.le ContinuousLinearEquiv.homothety_inverse le_refl mul_inv_cancel₀ ContinuousLinearMap.le_opNorm one_le_of_le_mul_right₀ MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono
exists_dual_vector' 📖	mathematical	—	Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing DenselyNormedField.toNontriviallyNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Real Real.instOne DFunLike.coe ContinuousLinearMap.funLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RCLike.ofReal NormedAddCommGroup.toNorm	—	exists_norm_ne_zero EMetric.instNontrivialTopologyOfNontrivial exists_dual_vector map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass norm_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass norm_ne_zero_iff
exists_dual_vector'' 📖	mathematical	—	Real Real.instLE Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing DenselyNormedField.toNontriviallyNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Real.instOne DFunLike.coe ContinuousLinearMap.funLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RCLike.ofReal SeminormedAddCommGroup.toNorm	—	norm_zero RingHomIsometric.ids Real.instZeroLEOneClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass exists_dual_vector Eq.le
exists_extension_norm_eq 📖	mathematical	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Subspace NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SetLike.instMembership Submodule.setLike DivisionRing.toDivisionSemiring instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module Norm.norm ContinuousLinearMap.hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing Submodule.normedSpace Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	RestrictScalars.isScalarTower RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Submodule.isScalarTower' IsScalarTower.left IsScalarTower.right Real.exists_extension_norm_eq ContinuousLinearMap.extendTo𝕜'_apply Submodule.coe_smul map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass mul_comm RCLike.mul_re RCLike.I_re MulZeroClass.mul_zero RCLike.I_im zero_sub map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass RCLike.charZero_rclike SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass neg_mul sub_neg_eq_add RCLike.re_add_im le_antisymm ContinuousLinearMap.norm_extendTo𝕜' ContinuousLinearMap.opNorm_comp_le RingHomIsometric.ids RCLike.reCLM_norm one_mul ContinuousLinearMap.opNorm_le_bound ContinuousLinearMap.opNorm_nonneg ContinuousLinearMap.le_opNorm

---

← Back to Index