Documentation Verification Report

InnerDual

📁 Source: Mathlib/Analysis/Convex/Cone/InnerDual.lean

Statistics

Metric	Count
Definitions `innerDual`	1
Theorems `hyperplane_separation_of_nonempty_of_isClosed_of_notMem`, `hyperplane_separation'`, `hyperplane_separation_of_notMem`, `innerDual_empty`, `innerDual_iUnion`, `innerDual_innerDual`, `innerDual_insert`, `innerDual_le_innerDual`, `innerDual_sUnion`, `innerDual_singleton`, `innerDual_toSubmodule`, `innerDual_union`, `innerDual_univ`, `innerDual_zero`, `mem_innerDual`, `relative_hyperplane_separation`	16
Total	17

ConvexCone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hyperplane_separation_of_nonempty_of_isClosed_of_notMem` 📖	mathematical	`Set.Nonempty` `SetLike.coe` `ConvexCone` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instSetLike` `SetLike.instMembership`	`Real.instLE` `Real.instZero` `Inner.inner` `InnerProductSpace.toInner` `Real.instLT`	—	`exists_norm_eq_iInf_of_complete_convex` `IsClosed.isComplete` `convex` `norm_eq_iInf_iff_real_inner_le_zero` `neg_sub` `one_smul` `neg_smul` `real_inner_smul_right` `neg_eq_neg_one_mul` `neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `real_inner_comm` `add_sub_cancel_right` `add_mem` `Pointed.of_nonempty_of_isClosed` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `sub_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₃` `neg_zero` `lt_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `neg_one_mul` `real_inner_smul_left` `smul_sub` `neg_sub_neg` `lt_of_not_ge` `Iff.not` `real_inner_self_nonpos` `add_zero` `add_le_add` `Eq.ge` `Right.neg_nonpos_iff` `inner_neg_right` `zero_sub` `inner_add_right` `sub_add_cancel`

ProperCone

Definitions

Name	Category	Theorems
`innerDual` 📖	CompOp	13 math math: `innerDual_le_innerDual`, `innerDual_univ`, `innerDual_sUnion`, `innerDual_zero`, `innerDual_singleton`, `innerDual_union`, `innerDual_insert`, `innerDual_empty`, `mem_innerDual`, `hyperplane_separation_of_notMem`, `innerDual_iUnion`, `innerDual_toSubmodule`, `innerDual_innerDual`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hyperplane_separation'` 📖	mathematical	`ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `SetLike.instMembership` `instSetLike`	`Real.instLE` `Real.instZero` `Inner.inner` `InnerProductSpace.toInner` `Real.instLT`	—	`Real.instIsOrderedRing` `hyperplane_separation_point` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `NormedSpace.toLocallyConvexSpace` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `real_inner_comm` `InnerProductSpace.toDual_symm_apply`
`hyperplane_separation_of_notMem` 📖	mathematical	`ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `SetLike.instMembership` `instSetLike` `map` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul`	`innerDual` `SetLike.coe` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `ContinuousLinearMap.adjoint` `Real.instLT` `Inner.inner` `InnerProductSpace.toInner`	—	`Real.instIsOrderedRing` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Mathlib.Tactic.Contrapose.contrapose₂` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `Mathlib.Tactic.Push.not_and_eq` `relative_hyperplane_separation`
`innerDual_empty` 📖	mathematical	—	`innerDual` `Set` `Set.instEmptyCollection` `Top.top` `ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `OrderTop.toTop` `Preorder.toLE` `ClosedSubmodule` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.semiring` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Nonneg.instModule` `ClosedSubmodule.instPartialOrder` `ClosedSubmodule.instOrderTop`	—	`ext` `Real.instIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `instIsEmptyFalse`
`innerDual_iUnion` 📖	mathematical	—	`innerDual` `Set.iUnion` `iInf` `ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `ClosedSubmodule.instInfSet` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.semiring` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Nonneg.instModule`	—	`ext` `Real.instIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `forall_swap`
`innerDual_innerDual` 📖	mathematical	—	`innerDual` `SetLike.coe` `ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instSetLike`	—	`Real.instIsOrderedRing` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Algebra.to_smulCommClass` `LinearMap.flip.instIsContPerfPair` `InnerProductSpace.instIsContPerfPairRealInnerₗOfCompleteSpace` `flip_innerₗ` `dual.congr_simp` `dual_flip_dual` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `NormedSpace.toLocallyConvexSpace`
`innerDual_insert` 📖	mathematical	—	`innerDual` `Set` `Set.instInsert` `ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `ClosedSubmodule.instInf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.semiring` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Nonneg.instModule` `Set.instSingletonSet`	—	`Real.instIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Set.insert_eq` `innerDual_union`
`innerDual_le_innerDual` 📖	mathematical	`Set` `Set.instHasSubset`	`ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `innerDual`	—	`Real.instIsOrderedRing`
`innerDual_sUnion` 📖	mathematical	—	`innerDual` `Set.sUnion` `InfSet.sInf` `ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `ClosedSubmodule.instInfSet` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.semiring` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Nonneg.instModule` `Set.image` `Set`	—	`ext` `Real.instIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `forall_swap`
`innerDual_singleton` 📖	mathematical	—	`innerDual` `Set` `Set.instSingletonSet` `comap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `Real.partialOrder` `Real.instIsOrderedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.funLike` `innerSL` `positive` `Real.semiring` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.normedField` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsStrictOrderedModule.toIsOrderedModule` `MulZeroClass.toSMulWithZero` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `HasSolidNorm.orderClosedTopology` `Real.normedAddCommGroup` `Real.lattice` `instHasSolidNormReal`	—	`ext` `Real.instIsOrderedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono`
`innerDual_toSubmodule` 📖	mathematical	—	`ClosedSubmodule.toSubmodule` `Real` `Preorder.toLE` `PartialOrder.toPreorder` `Real.partialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Real.semiring` `Nonneg.semiring` `IsOrderedRing.toZeroLEOneClass` `Real.instIsOrderedRing` `IsOrderedRing.toPosMulMono` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Nonneg.instModule` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `innerDual` `PointedCone.dual` `Real.commRing` `SeminormedAddCommGroup.toAddCommGroup` `innerₗ`	—	`IsOrderedRing.toZeroLEOneClass` `Real.instIsOrderedRing` `IsOrderedRing.toPosMulMono`
`innerDual_union` 📖	mathematical	—	`innerDual` `Set` `Set.instUnion` `ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `ClosedSubmodule.instInf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.semiring` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Nonneg.instModule`	—	`le_antisymm` `Real.instIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `le_inf`
`innerDual_univ` 📖	mathematical	—	`innerDual` `Set.univ` `Bot.bot` `ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `OrderBot.toBot` `Preorder.toLE` `ClosedSubmodule` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.semiring` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Nonneg.instModule` `ClosedSubmodule.instPartialOrder` `ClosedSubmodule.instOrderBot` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`le_antisymm` `Real.instIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `inner_self_eq_norm_sq_to_K` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `AddGroup.existsAddOfLE` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Set.mem_univ`
`innerDual_zero` 📖	mathematical	—	`innerDual` `Set` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Top.top` `ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `OrderTop.toTop` `Preorder.toLE` `ClosedSubmodule` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nonneg.semiring` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Nonneg.instModule` `ClosedSubmodule.instPartialOrder` `ClosedSubmodule.instOrderTop`	—	`ext` `Real.instIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `inner_zero_left`
`mem_innerDual` 📖	mathematical	—	`ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `SetLike.instMembership` `instSetLike` `innerDual` `Real.instLE` `Real.instZero` `Inner.inner` `InnerProductSpace.toInner`	—	`Real.instIsOrderedRing`
`relative_hyperplane_separation` 📖	mathematical	—	`ProperCone` `Real` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `SetLike.instMembership` `instSetLike` `map` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Real.instLE` `Inner.inner` `InnerProductSpace.toInner`	—	`Real.instIsOrderedRing` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `RingHomSurjective.ids` `Set.image_congr` `Submodule.mapsTo_smul_closure` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousLinearMap.adjoint_inner_right` `real_inner_comm` `ge_of_tendsto'` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Continuous.seqContinuous` `Continuous.inner` `continuous_id` `continuous_const` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `hyperplane_separation'` `subset_closure` `Set.mem_image_of_mem`

---

← Back to Index