mathlib documentation

analysis.convex.extreme

Extreme sets #

This file defines extreme sets and extreme points for sets in a real vector space.

References #

See chapter 8 of Convexity

TODO:

def is_extreme {E : Type u_1} [add_comm_group E] [module E] (A B : set E) :
Prop

A set B is extreme to a set A if B ⊆ A and all points of B only belong to open segments whose ends are in B.

Equations
theorem is_extreme.refl {E : Type u_1} [add_comm_group E] [module E] (A : set E) :
theorem is_extreme.trans {E : Type u_1} [add_comm_group E] [module E] {A B C : set E} (hAB : is_extreme A B) (hBC : is_extreme B C) :
theorem is_extreme.convex_diff {E : Type u_1} [add_comm_group E] [module E] {A B : set E} (hA : convex A) (hAB : is_extreme A B) :
convex (A \ B)
theorem is_extreme.inter {E : Type u_1} [add_comm_group E] [module E] {A B C : set E} (hAB : is_extreme A B) (hAC : is_extreme A C) :
is_extreme A (B C)
theorem is_extreme.Inter {E : Type u_1} [add_comm_group E] [module E] {A : set E} {ι : Type u_2} [nonempty ι] {F : ι → set E} (hAF : ∀ (i : ι), is_extreme A (F i)) :
is_extreme A (⋂ (i : ι), F i)
theorem is_extreme.bInter {E : Type u_1} [add_comm_group E] [module E] {A : set E} {F : set (set E)} (hF : F.nonempty) (hAF : ∀ (B : set E), B Fis_extreme A B) :
is_extreme A (⋂ (B : set E) (H : B F), B)
theorem is_extreme.sInter {E : Type u_1} [add_comm_group E] [module E] {A : set E} {F : set (set E)} (hF : F.nonempty) (hAF : ∀ (B : set E), B Fis_extreme A B) :
theorem is_extreme.mono {E : Type u_1} [add_comm_group E] [module E] {A B C : set E} (hAC : is_extreme A C) (hBA : B A) (hCB : C B) :
def set.extreme_points {E : Type u_1} [add_comm_group E] [module E] (A : set E) :
set E

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 open_segment x x.

Equations
theorem extreme_points_def {E : Type u_1} [add_comm_group E] [module E] {x : E} {A : set E} :
x A.extreme_points x A ∀ (x₁ x₂ : E), x₁ Ax₂ Ax open_segment x₁ x₂x₁ = x x₂ = x
theorem mem_extreme_points_iff_forall_segment {E : Type u_1} [add_comm_group E] [module E] {x : E} {A : set E} :
x A.extreme_points x A ∀ (x₁ x₂ : E), x₁ Ax₂ Ax segment x₁ x₂x₁ = x x₂ = x
theorem mem_extreme_points_iff_extreme_singleton {E : Type u_1} [add_comm_group E] [module E] {x : E} {A : set E} :

x is an extreme point to A iff {x} is an extreme set of A.

theorem extreme_points_subset {E : Type u_1} [add_comm_group E] [module E] {A : set E} :
@[simp]
theorem extreme_points_empty {E : Type u_1} [add_comm_group E] [module E] :
@[simp]
theorem extreme_points_singleton {E : Type u_1} [add_comm_group E] [module E] {x : E} :
theorem convex.mem_extreme_points_iff_convex_remove {E : Type u_1} [add_comm_group E] [module E] {x : E} {A : set E} (hA : convex A) :
x A.extreme_points x A convex (A \ {x})
theorem convex.mem_extreme_points_iff_mem_diff_convex_hull_remove {E : Type u_1} [add_comm_group E] [module E] {x : E} {A : set E} (hA : convex A) :
theorem is_extreme.extreme_points_eq {E : Type u_1} [add_comm_group E] [module E] {A B : set E} (hAB : is_extreme A B) :