Extreme

📁 Source: Mathlib/Analysis/Convex/Strict/Extreme.lean

Statistics

Metric	Count
Definitions	0
Theorems extremePoints_Icc, diff_interior_subset_extremePoints, extremePoints_eq_diff_interior, extremePoints_closedBall_eq_sphere, sphere_subset_extremePoints_closedBall, disjoint_interior_extremePoints, extremePoints_closedBall_subset_sphere	7
Total	7

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extremePoints_Icc 📖	mathematical	Real Real.instLE	extremePoints Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Icc Real.instPreorder Set instInsert instSingletonSet	—	Nat.instAtLeastTwoHAddOfNat Real.Icc_eq_closedBall StrictConvexSpace.extremePoints_closedBall_eq_sphere Real.instNontrivial Real.instStrictConvexSpace

StrictConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diff_interior_subset_extremePoints 📖	mathematical	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set Set.instHasSubset Set.instSDiff interior Set.extremePoints SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	one_smul add_smul
extremePoints_eq_diff_interior 📖	mathematical	StrictConvex Real Real.semiring Real.partialOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid 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	Set.extremePoints 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 Set Set.instSDiff interior	—	antisymm Set.instAntisymmSubset Set.subset_diff extremePoints_subset Disjoint.symm disjoint_interior_extremePoints SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul diff_interior_subset_extremePoints

StrictConvexSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extremePoints_closedBall_eq_sphere 📖	mathematical	—	Set.extremePoints 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 Metric.closedBall Metric.sphere	—	StrictConvex.extremePoints_eq_diff_interior strictConvex_closedBall interior_closedBall' Metric.closedBall_diff_ball
sphere_subset_extremePoints_closedBall 📖	mathematical	—	Set Set.instHasSubset Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.extremePoints Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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 Metric.closedBall	—	StrictConvex.diff_interior_subset_extremePoints strictConvex_closedBall Metric.closure_closedBall frontier.eq_1 frontier_closedBall

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_interior_extremePoints 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice interior Set.extremePoints 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.disjoint_iff Filter.Tendsto.eventually Filter.tendsto_inf_left Continuous.tendsto' continuous_sub_left IsTopologicalAddGroup.to_continuousSub sub_zero mem_interior_iff_mem_nhds continuous_const_add instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd add_zero Filter.Eventually.exists Real.punctured_nhds_module_neBot Filter.Eventually.and eventually_mem_nhdsWithin mem_openSegment_sub_add Real.instIsStrictOrderedRing IsStrictOrderedRing.toCharZero
extremePoints_closedBall_subset_sphere 📖	mathematical	—	Set Set.instHasSubset Set.extremePoints 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 Metric.closedBall Metric.sphere	—	Metric.closedBall_diff_ball Set.subset_diff interior_closedBall' extremePoints_subset Disjoint.symm disjoint_interior_extremePoints SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul

---

← Back to Index