Theorems · Theorem · convex and discrete geometry

mem_extremePoints

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E} {x : E},
  x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

A point x is an extreme point of a set A iff x ∈ A and for any x₁, x₂ such that x belongs to the open segment (x₁, x₂), we have x₁ = x and x₂ = x. We used to use the RHS as the definition of extremePoints. However, the conclusion x₂ = x is redundant, so we changed the definition to the RHS of mem_extremePoints_iff_left.

Defined in

Mathlib.Analysis.Convex.Extreme

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

SemiringPartialOrderAddCommMonoidSMul