Theorems · Definition · convex and discrete geometry
Set.extremePoints
(𝕜 : Type u_1) → {E : Type u_2} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → Set E → Set EA point x is an extreme point of a set A if x belongs to no open segment with ends in
A, except for the obvious openSegment x x.
- Defined in
- Mathlib.Analysis.Convex.Extreme
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- PartialOrderstatement and proof · cited by 6,410
- Set.ofPredproof · cited by 6,101
- openSegmentproof · cited by 102
Cited by43
Results whose statement or proof uses this declaration.
- extremePoints_subsetstatement and proof · cited by 8
- StrictConvex.sdiff_interior_subset_extremePointsstatement · cited by 3
- Convex.mem_extremePoints_iff_convex_sdiffstatement and proof · cited by 3
- Ergodic.of_mem_extremePoints_measure_univ_eqstatement and proof · cited by 2
- inter_extremePoints_subset_extremePoints_of_subsetstatement and proof · cited by 2
- disjoint_interior_extremePointsstatement and proof · cited by 2
- IsExtreme.extremePoints_subset_extremePointsstatement · cited by 2
- IsExtreme.mem_extremePointsstatement · cited by 2
- mem_extremePointsstatement and proof · cited by 2
- extremePoints_convexHull_subsetstatement and proof · cited by 2
- isExtreme_singletonstatement · cited by 2
- StrictConvex.extremePoints_eq_sdiff_interiorstatement · cited by 2