def faceRelativeInteriors (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : Set (Set (EuclideanSpace ℝ (Fin n)))

The collection 𝓤 of all relative interiors of nonempty convex faces of a convex set C in ℝⁿ.

Equations

• faceRelativeInteriors n C = {U : Set (EuclideanSpace ℝ (Fin n)) | ∃ (F : Set (EuclideanSpace ℝ (Fin n))), IsFace C F ∧ F.Nonempty ∧ Convex ℝ F ∧ U = euclideanRelativeInterior n F}

theorem euclideanRelativelyOpen_singleton (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) : euclideanRelativelyOpen n {x}

A singleton in ℝⁿ is relatively open.

theorem faceRelativeInteriors_eq_of_nonempty_inter {n : ℕ} {C U V : Set (EuclideanSpace ℝ (Fin n))} (hU : U ∈ faceRelativeInteriors n C) (hV : V ∈ faceRelativeInteriors n C) (hUV : (U ∩ V).Nonempty) : U = V

If two elements of faceRelativeInteriors meet, then they are equal.

theorem FaceOf.mem_sInf_iff {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {C : Set E} (hC : Convex 𝕜 C) (S : Set (FaceOf C)) {x : E} : x ∈ ↑(sInf C hC S) ↔ x ∈ C ∧ ∀ F ∈ S, x ∈ ↑F

Membership in FaceOf.sInf means lying in C and every face in S.

theorem maximizers_eq_inter_of_le {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (f : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ) {β : ℝ} (h_le : ∀ x ∈ C, f x ≤ β) (h_eq : ∃ x0 ∈ C, f x0 = β) : maximizers C f = C ∩ {x : EuclideanSpace ℝ (Fin n) | f x = β}

If a linear functional is bounded above by β on C and attains β, then its maximizers are exactly C ∩ {x | f x = β}.

theorem exists_faceRelativeInteriors_superset_of_relOpenConvex {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hC : Convex ℝ C) {D : Set (EuclideanSpace ℝ (Fin n))} (hDC : D ⊆ C) (hDconv : Convex ℝ D) (hDopen : euclideanRelativelyOpen n D) : ∃ U ∈ faceRelativeInteriors n C, D ⊆ U

Any relatively open convex subset of C is contained in a member of faceRelativeInteriors.

theorem faceRelativeInteriors_sUnion_eq {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hC : Convex ℝ C) : ⋃₀ faceRelativeInteriors n C = C

The union of faceRelativeInteriors is the ambient convex set.

theorem faceRelativeInteriors_maximal_of_absorption {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hC : Convex ℝ C) {U : Set (EuclideanSpace ℝ (Fin n))} (hU : U ∈ faceRelativeInteriors n C) {D : Set (EuclideanSpace ℝ (Fin n))} (hDC : D ⊆ C) (hDconv : Convex ℝ D) (hDopen : euclideanRelativelyOpen n D) (hUD : U ⊆ D) : D = U

Elements of faceRelativeInteriors are maximal relatively open convex subsets of C.

theorem faceRelativeInteriors_pairwiseDisjoint_and_sUnion_eq_and_maximal {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (hCne : C.Nonempty) (hC : Convex ℝ C) : (faceRelativeInteriors n C).Pairwise Disjoint ∧ ⋃₀ faceRelativeInteriors n C = C ∧ (∀ D ⊆ C, Convex ℝ D → euclideanRelativelyOpen n D → ∃ U ∈ faceRelativeInteriors n C, D ⊆ U) ∧ ∀ U ∈ faceRelativeInteriors n C, ∀ D ⊆ C, Convex ℝ D → euclideanRelativelyOpen n D → U ⊆ D → D = U

Theorem 18.2. Let C be a non-empty convex set, and let 𝓤 be the collection of all relative interiors of non-empty faces of C. Then 𝓤 is a partition of C (pairwise disjoint with union equal to C). Every relatively open convex subset of C is contained in some element of 𝓤, and the sets in 𝓤 are the maximal relatively open convex subsets of C.

theorem affineSpan_segment_eq_line {n : ℕ} (u v : EuclideanSpace ℝ (Fin n)) : affineSpan ℝ (segment ℝ u v) = affineSpan ℝ {u, v}

The affine span of a segment is the line through its endpoints.

theorem openSegment_subset_euclideanRelativeInterior_segment {n : ℕ} {u v : EuclideanSpace ℝ (Fin n)} (huv : u ≠ v) : openSegment ℝ u v ⊆ euclideanRelativeInterior n (segment ℝ u v)

Points in an open segment lie in the relative interior of the closed segment.

theorem den_two_between {t1 t2 : ℝ} (ht1 : t1 ∈ Set.Ioo 0 1) (ht2 : t2 ∈ Set.Ioo 0 1) : 0 < t1 + t2 - t1 * t2 ∧ t1 + t2 - t1 * t2 < 1

The denominator in the two-between computation lies in (0,1).

theorem lineMap_solve_y_of_two_between {n : ℕ} {x y u v : EuclideanSpace ℝ (Fin n)} {t1 t2 : ℝ} (hx : x = (AffineMap.lineMap y u) t1) (hy : y = (AffineMap.lineMap x v) t2) (hden : t1 + t2 - t1 * t2 ≠ 0) : y = (AffineMap.lineMap u v) (t2 / (t1 + t2 - t1 * t2))

Solve for y from two lineMap relations by eliminating the middle point.

theorem lineMap_solve_x_of_two_between {n : ℕ} {x y u v : EuclideanSpace ℝ (Fin n)} {t1 t2 : ℝ} (hx : x = (AffineMap.lineMap y u) t1) (hy : y = (AffineMap.lineMap x v) t2) (hden : t1 + t2 - t1 * t2 ≠ 0) : x = (AffineMap.lineMap u v) ((1 - t1) * t2 / (t1 + t2 - t1 * t2))

Solve for x from two lineMap relations by substituting the computed y.

theorem openSegment_of_two_between_relations {n : ℕ} {x y u v : EuclideanSpace ℝ (Fin n)} (hx : x ∈ openSegment ℝ y u) (hy : y ∈ openSegment ℝ x v) : x ∈ openSegment ℝ u v ∧ y ∈ openSegment ℝ u v

If x is between y and u, and y is between x and v, then both lie between u and v.

theorem dir2_implies_dir1_take_D_eq_ri_segment {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {x y u v : EuclideanSpace ℝ (Fin n)} (hsegC : segment ℝ u v ⊆ C) (hxri : x ∈ euclideanRelativeInterior n (segment ℝ u v)) (hyri : y ∈ euclideanRelativeInterior n (segment ℝ u v)) : ∃ D ⊆ C, Convex ℝ D ∧ euclideanRelativelyOpen n D ∧ x ∈ D ∧ y ∈ D

From a segment whose relative interior contains x,y, build a relatively open convex subset.

theorem dir1_implies_dir2_extend_past_x_and_y {n : ℕ} {C D : Set (EuclideanSpace ℝ (Fin n))} {x y : EuclideanSpace ℝ (Fin n)} (hDC : D ⊆ C) (hDconv : Convex ℝ D) (hDopen : euclideanRelativelyOpen n D) (hxD : x ∈ D) (hyD : y ∈ D) (hxy : x ≠ y) : ∃ (u : EuclideanSpace ℝ (Fin n)) (v : EuclideanSpace ℝ (Fin n)), u ≠ v ∧ segment ℝ u v ⊆ C ∧ x ∈ euclideanRelativeInterior n (segment ℝ u v) ∧ y ∈ euclideanRelativeInterior n (segment ℝ u v)

From a relatively open convex D, extend past x and y to get a segment in C.

theorem exists_relativelyOpenConvex_subset_iff_exists_segment_mem_relativeInterior {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {x y : EuclideanSpace ℝ (Fin n)} (hxy : x ≠ y) : (∃ D ⊆ C, Convex ℝ D ∧ euclideanRelativelyOpen n D ∧ x ∈ D ∧ y ∈ D) ↔ ∃ (u : EuclideanSpace ℝ (Fin n)) (v : EuclideanSpace ℝ (Fin n)), u ≠ v ∧ segment ℝ u v ⊆ C ∧ x ∈ euclideanRelativeInterior n (segment ℝ u v) ∧ y ∈ euclideanRelativeInterior n (segment ℝ u v)

Text 18.2.1. Let C be a convex set and let x, y be two distinct points in C. The following two conditions are equivalent:

(1) There exists a relatively open convex subset D ⊆ C such that x ∈ D and y ∈ D.

(2) There exists a line segment S ⊆ C such that both x and y belong to the relative interior of S (i.e. x, y ∈ ri(S)).

theorem mixedConvexHull_subset_of_convex_of_subset_of_recedes {n : ℕ} {S₀ S₁ Ccand : Set (Fin n → ℝ)} (hCconv : Convex ℝ Ccand) (hS₀ : S₀ ⊆ Ccand) (hrec : ∀ d ∈ S₁, ∀ x ∈ Ccand, ∀ (t : ℝ), 0 ≤ t → x + t • d ∈ Ccand) : mixedConvexHull S₀ S₁ ⊆ Ccand

A convex set containing S₀ and receding along S₁ contains the mixed convex hull.

theorem mem_recessionCone_mixedConvexHull_of_mem_directions {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hd : d ∈ S₁) : d ∈ (mixedConvexHull S₀ S₁).recessionCone

Directions in S₁ are recession directions of the mixed convex hull.

theorem isFace_image_equiv_fin {n : ℕ} {C C' : Set (Fin n → ℝ)} (hC' : IsFace C C') : IsFace (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C')

Transport a face along the EuclideanSpace equivalence.

theorem isFace_eq_inter_closure_fin {n : ℕ} {C C' : Set (Fin n → ℝ)} (hC' : IsFace C C') (hC'conv : Convex ℝ C') : C' = C ∩ closure C'

Faces in Fin n → ℝ satisfy C' = C ∩ closure C'.

theorem mem_recessionCone_face_of_mem_recessionCone_of_mem_recessionCone_closure {n : ℕ} {S₀ S₁ C' : Set (Fin n → ℝ)} (hC' : IsFace (mixedConvexHull S₀ S₁) C') (hC'conv : Convex ℝ C') {d : Fin n → ℝ} (hdC : d ∈ (mixedConvexHull S₀ S₁).recessionCone) (hdCl : d ∈ (closure C').recessionCone) : d ∈ C'.recessionCone

If a direction recedes in both C and closure C', it recedes in the face C'.

theorem mem_recessionCone_closure_of_exists_ray {n : ℕ} {K : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hKconv : Convex ℝ K) (hRay : ∃ x0 ∈ K, ∀ (t : ℝ), 0 ≤ t → x0 + t • d ∈ K) : d ∈ (closure K).recessionCone

A ray in a convex set gives a recession direction of its closure.

theorem mixedConvexHull_mono {n : ℕ} {S₀ S₁ T₀ T₁ : Set (Fin n → ℝ)} (hS₀ : S₀ ⊆ T₀) (hS₁ : S₁ ⊆ T₁) : mixedConvexHull S₀ S₁ ⊆ mixedConvexHull T₀ T₁

Monotonicity of the mixed convex hull in both arguments.