Separation

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

Statistics

Metric	Count
Definitions	0
Theorems geometric_hahn_banach_closed_compact, geometric_hahn_banach_closed_point, geometric_hahn_banach_compact_closed, geometric_hahn_banach_of_nonempty_interior, geometric_hahn_banach_of_nonempty_interior', geometric_hahn_banach_of_nonempty_interior_point, geometric_hahn_banach_open, geometric_hahn_banach_open_open, geometric_hahn_banach_open_point, geometric_hahn_banach_point_closed, geometric_hahn_banach_point_open, geometric_hahn_banach_point_point, iInter_countable_halfSpaces_eq, iInter_halfSpaces_eq, iInter_halfSpaces_eq', separate_convex_open_set, geometric_hahn_banach_closed_compact, geometric_hahn_banach_closed_point, geometric_hahn_banach_compact_closed, geometric_hahn_banach_of_nonempty_interior, geometric_hahn_banach_of_nonempty_interior', geometric_hahn_banach_of_nonempty_interior_point, geometric_hahn_banach_open, geometric_hahn_banach_open_open, geometric_hahn_banach_open_point, geometric_hahn_banach_point_closed, geometric_hahn_banach_point_open, geometric_hahn_banach_point_point, iInter_halfSpaces_eq, separate_convex_open_set	30
Total	30

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geometric_hahn_banach_closed_compact 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsCompact Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_compact_closed Disjoint.symm SeminormedAddCommGroup.toIsTopologicalAddGroup map_neg AddMonoidHom.instAddMonoidHomClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add
geometric_hahn_banach_closed_point 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_closed_compact convex_singleton isCompact_singleton Set.disjoint_singleton_right LT.lt.trans Set.mem_singleton
geometric_hahn_banach_compact_closed 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsCompact Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	IsScalarTower.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul geometric_hahn_banach_compact_closed RingHomInvPair.ids IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsScalarTower.to_smulCommClass' IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousSMul.continuousConstSMul StrongDual.extendRCLikeₗ_apply StrongDual.re_extendRCLike_apply
geometric_hahn_banach_of_nonempty_interior 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice interior Set.Nonempty	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLE DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	IsScalarTower.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul geometric_hahn_banach_of_nonempty_interior RingHomInvPair.ids IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsScalarTower.to_smulCommClass' IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousSMul.continuousConstSMul LinearEquiv.injective map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass EquivLike.toEmbeddingLike StrongDual.extendRCLikeₗ_apply StrongDual.re_extendRCLike_apply
geometric_hahn_banach_of_nonempty_interior' 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice interior Set.Nonempty	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLE DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_of_nonempty_interior map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass instReflLe
geometric_hahn_banach_of_nonempty_interior_point 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership interior Set.Nonempty	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLE DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	IsScalarTower.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul geometric_hahn_banach_of_nonempty_interior_point RingHomInvPair.ids IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsScalarTower.to_smulCommClass' IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousSMul.continuousConstSMul LinearEquiv.injective map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass EquivLike.toEmbeddingLike StrongDual.extendRCLikeₗ_apply StrongDual.re_extendRCLike_apply
geometric_hahn_banach_open 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instLE	—	IsScalarTower.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul geometric_hahn_banach_open RingHomInvPair.ids IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsScalarTower.to_smulCommClass' IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousSMul.continuousConstSMul StrongDual.extendRCLikeₗ_apply StrongDual.re_extendRCLike_apply
geometric_hahn_banach_open_open 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	IsScalarTower.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul geometric_hahn_banach_open_open RingHomInvPair.ids IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsScalarTower.to_smulCommClass' IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousSMul.continuousConstSMul StrongDual.extendRCLikeₗ_apply StrongDual.re_extendRCLike_apply
geometric_hahn_banach_open_point 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen Set Set.instMembership	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	IsScalarTower.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul geometric_hahn_banach_open_point RingHomInvPair.ids IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsScalarTower.to_smulCommClass' IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousSMul.continuousConstSMul StrongDual.extendRCLikeₗ_apply StrongDual.re_extendRCLike_apply
geometric_hahn_banach_point_closed 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_compact_closed convex_singleton isCompact_singleton Set.disjoint_singleton_left LT.lt.trans' Set.mem_singleton
geometric_hahn_banach_point_open 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen Set Set.instMembership	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_open_point SeminormedAddCommGroup.toIsTopologicalAddGroup map_neg AddMonoidHom.instAddMonoidHomClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add
geometric_hahn_banach_point_point 📖	mathematical	—	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real Real.instLT DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_compact_closed convex_singleton isCompact_singleton isClosed_singleton Set.disjoint_singleton lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le
iInter_countable_halfSpaces_eq 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	Set.iInter setOf Real Real.instLE DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Subtype.prop map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass instReflLe Set.iInter_sigma Set.iInter_subtype Set.iInter_congr_Prop iInter_halfSpaces_eq' eq_closed_inter_nat isClosed_le HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Continuous.comp continuous_re ContinuousLinearMap.continuous continuous_const
iInter_halfSpaces_eq 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	Set.iInter StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid setOf Set Set.instMembership Real Real.instLE DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Set.iInter_setOf Set.Subset.antisymm geometric_hahn_banach_closed_point LT.lt.false LT.lt.trans LE.le.trans_lt le_rfl
iInter_halfSpaces_eq' 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	Set.iInter StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid Real setOf Real.instLE DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Set.iInter_setOf Set.Subset.antisymm geometric_hahn_banach_closed_point LT.lt.false LT.lt.trans_le LT.lt.le
separate_convex_open_set 📖	mathematical	Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instOne Real.instLT	—	IsScalarTower.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul separate_convex_open_set RingHomInvPair.ids IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsScalarTower.to_smulCommClass' IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousSMul.continuousConstSMul StrongDual.extendRCLikeₗ_apply StrongDual.re_extendRCLike_apply

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geometric_hahn_banach_closed_compact 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsCompact Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_compact_closed Disjoint.symm instIsTopologicalAddGroupReal IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add
geometric_hahn_banach_closed_point 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_closed_compact convex_singleton isCompact_singleton Set.disjoint_singleton_right LT.lt.trans Set.mem_singleton
geometric_hahn_banach_compact_closed 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsCompact Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Set.eq_empty_or_nonempty Nat.instAtLeastTwoHAddOfNat IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid instIsEmptyFalse IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add Real.instZeroLEOneClass RCLike.charZero_rclike NeZero.charZero_one Disjoint.exists_open_convexes Real.instIsStrictOrderedRing ContinuousSMul.continuousConstSMul geometric_hahn_banach_open_open IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Continuous.continuousOn ContinuousLinearMap.continuous lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.CancelDenoms.div_subst Mathlib.Tactic.CancelDenoms.add_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq
geometric_hahn_banach_of_nonempty_interior 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice interior Set.Nonempty	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLE DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_open Convex.interior ContinuousSMul.continuousConstSMul Real.instZeroLEOneClass isOpen_interior Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le closure_minimal le_of_lt IsClosed.preimage ContinuousLinearMap.continuous isClosed_Iic instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Convex.closure_interior_eq_closure_of_nonempty_interior instOrderTopologyReal subset_closure
geometric_hahn_banach_of_nonempty_interior' 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice interior Set.Nonempty	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLE DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_of_nonempty_interior instReflLe
geometric_hahn_banach_of_nonempty_interior_point 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership interior Set.Nonempty	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLE DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_of_nonempty_interior convex_singleton Set.disjoint_singleton_right Set.singleton_nonempty LE.le.trans Set.mem_singleton
geometric_hahn_banach_open 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instLE	—	Set.eq_empty_or_nonempty le_rfl zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike instIsEmptyFalse Set.sub_mem_sub sub_add_sub_cancel' sub_self Convex.vadd Convex.sub Disjoint.zero_notMem_sub_set Set.vadd_mem_vadd_set_iff add_zero separate_convex_open_set IsOpen.vadd SeparatelyContinuousAdd.to_continuousVAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd IsOpen.sub_right Set.vadd_mem_vadd_set le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing ContinuousLinearMap.map_add ContinuousLinearMap.map_sub Set.image_subset_iff interior_Iic instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMaxOrderOfNontrivial Real.instNontrivial interior_maximal le_csInf Set.Nonempty.image Set.forall_mem_image ContinuousLinearMap.isOpenMap_of_ne_zero IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal csInf_le Set.mem_image_of_mem
geometric_hahn_banach_open_open 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Set.eq_empty_or_nonempty IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid instIsEmptyFalse Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike geometric_hahn_banach_open Set.image_subset_iff interior_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial interior_maximal ContinuousLinearMap.isOpenMap_of_ne_zero IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal IsTopologicalAddGroup.toContinuousAdd LT.lt.not_ge
geometric_hahn_banach_open_point 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen Set Set.instMembership	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_open convex_singleton Set.disjoint_singleton_right lt_of_lt_of_le Set.mem_singleton
geometric_hahn_banach_point_closed 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_compact_closed convex_singleton isCompact_singleton Set.disjoint_singleton_left LT.lt.trans' Set.mem_singleton
geometric_hahn_banach_point_open 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen Set Set.instMembership	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_open_point instIsTopologicalAddGroupReal IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add
geometric_hahn_banach_point_point 📖	mathematical	—	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.instLT DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	geometric_hahn_banach_compact_closed convex_singleton isCompact_singleton isClosed_singleton Set.disjoint_singleton lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le
iInter_halfSpaces_eq 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	Set.iInter StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid setOf Set Set.instMembership Real.instLE DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Set.iInter_setOf Set.Subset.antisymm geometric_hahn_banach_closed_point LT.lt.not_ge LT.lt.trans LE.le.trans_lt le_rfl
separate_convex_open_set 📖	mathematical	Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen	StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instOne Real.instLT	—	exists_extension_of_le_sublinear gauge_smul_of_nonneg Real.instIsStrictOrderedRing IsStrictOrderedRing.toIsStrictOrderedModule Set.isScalarTower IsScalarTower.left LT.lt.le gauge_add_le absorbent_nhds_zero IsOpen.mem_nhds Submodule.mem_span_singleton LinearPMap.mkSpanSingleton'_apply mul_one le_or_gt LE.le.trans gauge_nonneg smul_eq_mul le_mul_iff_one_le_right IsOrderedRing.toPosMulMono Real.instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono one_le_gauge_of_notMem Convex.starConvex Absorbent.absorbs Submodule.mem_span_singleton_self LinearPMap.mkSpanSingleton'_apply_self LE.le.trans_lt gauge_lt_one_of_mem_of_isOpen LinearMap.continuous_of_nonzero_on_open IsOpen.vadd SeparatelyContinuousAdd.to_continuousVAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd Set.Nonempty.vadd_set Set.vadd_set_subset_iff map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.lt_of_eq_of_lt neg_eq_zero sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt

---

← Back to Index