KreinMilman

📁 Source: Mathlib/Analysis/Convex/KreinMilman.lean

Statistics

Metric	Count
Definitions	0
Theorems extremePoints_nonempty, closure_convexHull_extremePoints, surjOn_extremePoints_image	3
Total	3

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extremePoints_nonempty 📖	mathematical	IsCompact Set.Nonempty	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	—	zorn_superset Set.eq_empty_or_nonempty isClosed IsExtreme.rfl Set.sInter_eq_iInter nonempty_iInter_of_directed_nonempty_isCompact_isClosed Set.Nonempty.to_subtype IsChain.total Set.instReflSubset Subtype.mem Set.Subset.rfl of_isClosed_subset IsExtreme.subset isClosed_sInter isExtreme_sInter Set.sInter_subset_of_mem Minimal.prop IsExtreme.mem_extremePoints Set.eq_singleton_iff_unique_mem geometric_hahn_banach_point_point T2Space.t1Space exists_isMaxOn instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.continuousOn ContinuousLinearMap.continuous LT.lt.not_ge Minimal.eq_of_ge IsExposed.isClosed IsExtreme.trans IsExposed.isExtreme Real.instIsStrictOrderedRing Set.sep_subset

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_convexHull_extremePoints 📖	mathematical	IsCompact 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	closure DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.extremePoints	—	HasSubset.Subset.antisymm Set.instAntisymmSubset closure_minimal convexHull_min extremePoints_subset IsCompact.isClosed Set.not_subset geometric_hahn_banach_closed_point Convex.closure ContinuousSMul.continuousConstSMul convex_convexHull isClosed_closure IsCompact.exists_isMaxOn instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.continuousOn ContinuousLinearMap.continuous IsCompact.extremePoints_nonempty IsExposed.isCompact 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_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing subset_closure subset_convexHull IsExtreme.extremePoints_subset_extremePoints IsExposed.isExtreme Mathlib.Tactic.Linarith.sub_nonpos_of_le
surjOn_extremePoints_image 📖	mathematical	IsCompact	Set.SurjOn DFunLike.coe ContinuousAffineMap Real Real.instRing addGroupIsAddTorsor AddCommGroup.toAddGroup ContinuousAffineMap.instFunLike Set.extremePoints Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set.image	—	IsCompact.inter_right IsClosed.preimage ContinuousAffineMap.continuous isClosed_singleton extremePoints_subset IsCompact.extremePoints_nonempty Set.mem_image_of_mem Set.image_congr image_openSegment covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mem_extremePoints

---

← Back to Index