SeparatingDual

📁 Source: Mathlib/Analysis/LocallyConvex/SeparatingDual.lean

Statistics

Metric	Count
Definitions	0
Theorems instContinuousLinearMap, conjContinuousAlgEquiv_ext_iff, dualMap_surjective_iff, exists_continuousLinearEquiv_apply_eq, exists_eq_one, exists_eq_one_ne_zero_of_ne_zero_pair, exists_ne_zero, exists_ne_zero', exists_separating_of_ne, instNontrivialContinuousLinearMapIdOfContinuousSMul, t1Space, t2Space, instSeparatingDual, instSeparatingDualRealOfIsTopologicalAddGroupOfContinuousSMulOfLocallyConvexSpaceOfT1Space, separatingDual_def, separatingDual_iff_injective	16
Total	16

Algebra.IsCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousLinearMap 📖	mathematical	—	Algebra.IsCentral ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.algebra Algebra.toSMul	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Subalgebra.center_eq_top Unique.instSubsingleton Nontrivial.to_nonempty IsLocalRing.toNontrivial Field.instIsLocalRing exists_ne SeparatingDual.exists_eq_one IsScalarTower.left one_smul Subalgebra.mem_center_iff center_eq_bot algebraMap_smul ContinuousLinearMap.isScalarTower

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjContinuousAlgEquiv_ext_iff 📖	mathematical	—	conjContinuousAlgEquiv ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Units ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instSMulUnitsId AddCommMonoid.toAddMonoid smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.left	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left ContinuousSMul.continuousConstSMul RingHomCompTriple.ids ContinuousLinearMap.comp_assoc Subalgebra.mem_center_iff Algebra.IsCentral.center_eq_bot Algebra.IsCentral.instContinuousLinearMap Algebra.IsCentral.self Algebra.algebraMap_eq_smul_one zero_smul EquivLike.toEmbeddingLike AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousSemilinearEquivClass.continuousSemilinearMapClass continuousSemilinearEquivClass map_zero smul_zero map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousLinearMap.ext symm_apply_apply

SeparatingDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dualMap_surjective_iff 📖	mathematical	—	ContinuousLinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Module.Dual DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.dualMap ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	smulCommClass_self LinearMap.dualMap_surjective_iff Function.Surjective.of_comp IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring Algebra.to_smulCommClass SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul SMulCommClass.symm separatingDual_iff_injective IsTopologicalRing.to_topologicalAddGroup RingHomCompTriple.ids LinearMap.flip_surjective_iff₁ LinearMap.coe_comp
exists_continuousLinearEquiv_apply_eq 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	RingHomInvPair.ids exists_eq_one_ne_zero_of_ne_zero_pair map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass add_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg map_smul SemilinearMapClass.toMulActionSemiHomClass smul_add smul_smul MulActionSemiHomClass.map_smulₛₗ map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass mul_sub mul_one add_sub_cancel mul_comm mul_assoc inv_mul_cancel₀ smul_sub one_mul Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_inv₀ RingHomClass.toMonoidWithZeroHomClass mul_inv_cancel₀ Continuous.fun_add IsTopologicalAddGroup.toContinuousAdd continuous_id' Continuous.smul ContinuousLinearMap.continuous continuous_const Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Continuous.prodMk one_smul
exists_eq_one 📖	mathematical	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	exists_ne_zero Algebra.to_smulCommClass SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring inv_mul_cancel₀
exists_eq_one_ne_zero_of_ne_zero_pair 📖	mathematical	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	exists_eq_one ne_or_eq Algebra.to_smulCommClass SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring inv_mul_cancel₀ mul_one IsTopologicalSemiring.toContinuousAdd add_zero zero_add NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing
exists_ne_zero 📖	—	—	—	—	exists_ne_zero'
exists_ne_zero' 📖	—	—	—	—	—
exists_separating_of_ne 📖	—	—	—	—	exists_ne_zero sub_ne_zero_of_ne map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
instNontrivialContinuousLinearMapIdOfContinuousSMul 📖	mathematical	—	Nontrivial ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid	—	exists_ne exists_ne_zero IsScalarTower.left DFunLike.ne_iff
t1Space 📖	mathematical	—	T1Space	—	t1Space_iff_exists_open exists_separating_of_ne IsOpen.preimage ContinuousLinearMap.continuous isOpen_compl_singleton
t2Space 📖	mathematical	—	T2Space	—	t2Space_iff exists_separating_of_ne separated_by_continuous ContinuousLinearMap.continuous

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSeparatingDual 📖	mathematical	—	SeparatingDual NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedSpace.toModule	—	RestrictScalars.isScalarTower NormedSpace.toLocallyConvexSpace' map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass RCLike.geometric_hahn_banach_point_point SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
instSeparatingDualRealOfIsTopologicalAddGroupOfContinuousSMulOfLocallyConvexSpaceOfT1Space 📖	mathematical	—	SeparatingDual Real Real.instRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	geometric_hahn_banach_point_point LT.lt.ne' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
separatingDual_def 📖	mathematical	—	SeparatingDual	—	—
separatingDual_iff_injective 📖	mathematical	—	SeparatingDual DivisionRing.toRing Field.toDivisionRing LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toModule ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring ContinuousLinearMap.module Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring 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 DFunLike.coe LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm LinearMap.instFunLike LinearMap.flip ContinuousLinearMap.coeLM	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring Algebra.to_smulCommClass SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul SMulCommClass.symm DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass not_imp_comm LinearMap.ext_iff

---

← Back to Index