Convexity

DefinitionConvex subsets#

Convexity of sets.

Convex.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E]
  [SMul 𝕜 E] (s : Set E) : Prop

Sources

• Mathlib documentation: Convex
• Source of Convex in Mathlib/Analysis/Convex/Basic.lean
• Mathlib undergraduate list: Affine and Euclidean Geometry › Convexity

MathlibConvex

Uses 1 · Used by 24

Statement usesNatural number

Used byLiouville’s Theorem and the Construction of Transcendental Numbers · Minkowski’s Fundamental Theorem · L’Hopital’s Rule · Convex function · Local convexity · Boundary of a manifold · Integral curves · Interior of a manifold · Lie algebra of a Lie group · Pullback of vector fields · Smooth immersion · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners) · Tangent bundle · Covariant derivatives · (smooth) vector bundle · Darboux's theorem (analysis) · Open mapping theorem (complex analysis) · Akra–Bazzi theorem · Helly's theorem · Convex hull of a subset of an affine real space · Partial derivatives commute · Differentiability of the limit of a sequence of functions · Hilbert projection theorem

DefinitionConvex hull of a subset of an affine real space#

The convex hull of a set s is the minimal convex set that includes s.

convexHull.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E]
  [_root_.Module 𝕜 E] : ClosureOperator (Set E)

Sources

• Mathlib documentation: convexHull
• Source of convexHull in Mathlib/Analysis/Convex/Hull.lean
• Mathlib undergraduate list: Affine and Euclidean Geometry › Convexity

MathlibconvexHull

Uses 2 · Used by 6

Statement usesConvex subsets · Module

Used byCarathéodory's theorem · Birkhoff–Von Neumann theorem · Gauss–Lucas theorem · Krein–Milman theorem · Radon's theorem · Continuity (continuity and differentiability of convex functions)

DefinitionExtreme point#

A 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.

Set.extremePoints.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜]
  [AddCommMonoid E] [SMul 𝕜 E] (A : Set E) : Set E

Sources

• Mathlib documentation: Set.extremePoints
• Source of Set.extremePoints in Mathlib/Analysis/Convex/Extreme.lean
• Mathlib undergraduate list: Affine and Euclidean Geometry › Convexity

MathlibSet.extremePoints

Uses 1 · Used by 1

Statement usesNatural number

Used byKrein–Milman theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.