theorem convex_euclideanRelativeInterior (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) : Convex ℝ (euclideanRelativeInterior n C)

The relative interior of a convex set is convex.

theorem affineSpan_closure_eq (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : affineSpan ℝ (closure C) = affineSpan ℝ C

The affine span of the closure equals the affine span of the set.

theorem intrinsicInterior_subset_euclideanRelativeInterior (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : intrinsicInterior ℝ C ⊆ euclideanRelativeInterior n C

The intrinsic interior is contained in the Euclidean relative interior.

theorem affineSpan_intrinsicInterior_eq (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hCne : C.Nonempty) : affineSpan ℝ (intrinsicInterior ℝ C) = affineSpan ℝ C

The affine span of the intrinsic interior equals the affine span of a nonempty convex set.

theorem euclideanRelativeInterior_closure_convex_affineSpan (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) : Convex ℝ (closure C) ∧ Convex ℝ (euclideanRelativeInterior n C) ∧ affineSpan ℝ (closure C) = affineSpan ℝ C ∧ affineSpan ℝ (euclideanRelativeInterior n C) = affineSpan ℝ C ∧ (C.Nonempty → (euclideanRelativeInterior n C).Nonempty)

Theorem 6.2: Let C be a convex set in R^n. Then cl C and ri C are convex sets having the same affine hull (hence the same dimension) as C. In particular, ri C ≠ ∅ if C ≠ ∅.

theorem euclidean_closure_subset_closure_relativeInterior_of_nonempty (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hCne : C.Nonempty) : closure C ⊆ closure (euclideanRelativeInterior n C)

For a nonempty convex set, cl C is contained in cl (ri C).

theorem euclideanRelativeInterior_subset_relativeInterior_closure (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : euclideanRelativeInterior n C ⊆ euclideanRelativeInterior n (closure C)

The relative interior is monotone with respect to closure.

theorem euclideanRelativeInterior_closure_subset_relativeInterior (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hCne : C.Nonempty) : euclideanRelativeInterior n (closure C) ⊆ euclideanRelativeInterior n C

For a nonempty convex set, ri (cl C) is contained in ri C.

theorem euclidean_closure_relativeInterior_eq_and_relativeInterior_closure_eq (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) : closure (euclideanRelativeInterior n C) = closure C ∧ euclideanRelativeInterior n (closure C) = euclideanRelativeInterior n C

Theorem 6.3: For any convex set C in R^n, cl (ri C) = cl C and ri (cl C) = ri C.

theorem euclideanRelativeInterior_eq_of_closure_eq (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : closure C1 = closure C2 → euclideanRelativeInterior n C1 = euclideanRelativeInterior n C2

Closure equality for convex sets yields equality of relative interiors.

theorem euclidean_closure_eq_of_relativeInterior_eq (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : euclideanRelativeInterior n C1 = euclideanRelativeInterior n C2 → closure C1 = closure C2

Relative interior equality for convex sets yields equality of closures.

theorem euclidean_between_of_closure_eq (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : closure C1 = closure C2 → euclideanRelativeInterior n C1 ⊆ C2 ∧ C2 ⊆ closure C1

Closure equality yields a relative interior and closure sandwich.

theorem euclidean_closure_eq_of_between (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1 : Convex ℝ C1) : euclideanRelativeInterior n C1 ⊆ C2 ∧ C2 ⊆ closure C1 → closure C1 = closure C2

A relative interior and closure sandwich yields equality of closures.

theorem euclidean_closure_eq_iff_relativeInterior_eq_and_between (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : (closure C1 = closure C2 ↔ euclideanRelativeInterior n C1 = euclideanRelativeInterior n C2) ∧ (closure C1 = closure C2 ↔ euclideanRelativeInterior n C1 ⊆ C2 ∧ C2 ⊆ closure C1)

Corollary 6.3.1: Let C1 and C2 be convex sets in R^n. Then cl C1 = cl C2 if and only if ri C1 = ri C2. These conditions are equivalent to ri C1 ⊆ C2 ⊆ cl C1.

theorem euclidean_open_meets_closure_meets_relativeInterior (n : ℕ) (C U : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hU : IsOpen U) : (U ∩ closure C).Nonempty → (U ∩ euclideanRelativeInterior n C).Nonempty

Corollary 6.3.2. If C is a convex set in R^n, then every open set which meets cl C also meets ri C.

theorem affineSpan_le_of_subset_relativeBoundary (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1sub : C1 ⊆ euclideanRelativeBoundary n C2) : affineSpan ℝ C1 ≤ affineSpan ℝ C2

A subset of the relative boundary has affine span contained in the ambient affine span.

theorem affineSpan_eq_of_nonempty_of_finrank_eq (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1ne : C1.Nonempty) (hspan : affineSpan ℝ C1 ≤ affineSpan ℝ C2) (hfin : Module.finrank ℝ ↥(affineSpan ℝ C1).direction = Module.finrank ℝ ↥(affineSpan ℝ C2).direction) : affineSpan ℝ C1 = affineSpan ℝ C2

Equal direction finrank and nonempty inclusion forces equality of affine spans.

theorem ri_point_not_mem_closure_ri_of_disjoint (n : ℕ) {C1 C2 : Set (EuclideanSpace ℝ (Fin n))} {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ euclideanRelativeInterior n C1) (hspan : affineSpan ℝ C1 = affineSpan ℝ C2) (hdisj : Disjoint C1 (euclideanRelativeInterior n C2)) : x ∉ closure (euclideanRelativeInterior n C2)

A relative interior point cannot lie in the closure of a disjoint relative interior.

theorem euclidean_dim_lt_of_convex_subset_relativeBoundary (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) (hC1ne : C1.Nonempty) (hC2ne : C2.Nonempty) (hC1sub : C1 ⊆ euclideanRelativeBoundary n C2) : Module.finrank ℝ ↥(affineSpan ℝ C1).direction < Module.finrank ℝ ↥(affineSpan ℝ C2).direction

Corollary 6.3.3. If C1 is a non-empty convex subset of the relative boundary of a non-empty convex set C2 in R^n, then dim C1 < dim C2.

theorem euclideanRelativeInterior_exists_extension_point (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) {z : EuclideanSpace ℝ (Fin n)} (hz : z ∈ euclideanRelativeInterior n C) (x : EuclideanSpace ℝ (Fin n)) : x ∈ C → ∃ μ > 1, (1 - μ) • x + μ • z ∈ C

A relative interior point allows extending any segment past it inside C.

theorem euclideanRelativeInterior_iff_forall_exists_affine_combination_mem (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hCne : C.Nonempty) (z : EuclideanSpace ℝ (Fin n)) : z ∈ euclideanRelativeInterior n C ↔ ∀ x ∈ C, ∃ μ > 1, (1 - μ) • x + μ • z ∈ C

Theorem 6.4: Let C be a non-empty convex set in R^n. Then z ∈ ri C if and only if, for every x ∈ C, there exists μ > 1 such that (1 - μ) x + μ z belongs to C.

theorem interior_imp_forall_exists_add_smul_mem (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (z : EuclideanSpace ℝ (Fin n)) : z ∈ interior C → ∀ (y : EuclideanSpace ℝ (Fin n)), ∃ ε > 0, z + ε • y ∈ C

Interior points allow stepping a positive distance in any direction.

theorem forall_exists_add_smul_mem_imp_extension (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (z : EuclideanSpace ℝ (Fin n)) (h : ∀ (y : EuclideanSpace ℝ (Fin n)), ∃ ε > 0, z + ε • y ∈ C) (x : EuclideanSpace ℝ (Fin n)) : x ∈ C → ∃ μ > 1, (1 - μ) • x + μ • z ∈ C

Stepping in every direction yields the extension property of Theorem 6.4.

theorem affineSpan_eq_univ_of_forall_exists_add_smul_mem (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (z : EuclideanSpace ℝ (Fin n)) (h : ∀ (y : EuclideanSpace ℝ (Fin n)), ∃ ε > 0, z + ε • y ∈ C) : ↑(affineSpan ℝ C) = Set.univ

Stepping in every direction forces the affine span of C to be all of R^n.

theorem euclidean_interior_iff_forall_exists_add_smul_mem (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (z : EuclideanSpace ℝ (Fin n)) : z ∈ interior C ↔ ∀ (y : EuclideanSpace ℝ (Fin n)), ∃ ε > 0, z + ε • y ∈ C

Corollary 6.4.1: Let C be a convex set in R^n. Then z ∈ int C if and only if, for every y ∈ R^n, there exists ε > 0 such that z + ε y ∈ C.

theorem iInter_closure_subset_closure_iInter_relativeInterior (n : ℕ) {I : Type u_1} (C : I → Set (EuclideanSpace ℝ (Fin n))) (hC : ∀ (i : I), Convex ℝ (C i)) (hri : (⋂ (i : I), euclideanRelativeInterior n (C i)).Nonempty) : ⋂ (i : I), closure (C i) ⊆ closure (⋂ (i : I), euclideanRelativeInterior n (C i))

Points in all closures lie in the closure of the intersection of relative interiors.

theorem affine_combination_mem_of_between (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) {x z : EuclideanSpace ℝ (Fin n)} (hz : z ∈ C) {μ0 μ : ℝ} (hμ0 : 1 < μ0) (hμ1 : 1 ≤ μ) (hμ : μ ≤ μ0) (hμ0mem : (1 - μ0) • x + μ0 • z ∈ C) : (1 - μ) • x + μ • z ∈ C

Shrinking the extension parameter preserves membership in a convex set.

theorem exists_mu_gt_one_mem_iInter_of_finite (n : ℕ) {I : Type u_1} [Finite I] (C : I → Set (EuclideanSpace ℝ (Fin n))) (hC : ∀ (i : I), Convex ℝ (C i)) {x z : EuclideanSpace ℝ (Fin n)} (hz : z ∈ ⋂ (i : I), euclideanRelativeInterior n (C i)) (hx : x ∈ ⋂ (i : I), C i) : ∃ μ > 1, (1 - μ) • x + μ • z ∈ ⋂ (i : I), C i

A uniform extension parameter exists in a finite intersection of convex sets.

theorem euclidean_closure_iInter_eq_iInter_closure_of_common_relativeInterior (n : ℕ) {I : Type u_1} (C : I → Set (EuclideanSpace ℝ (Fin n))) (hC : ∀ (i : I), Convex ℝ (C i)) (hri : (⋂ (i : I), euclideanRelativeInterior n (C i)).Nonempty) : closure (⋂ (i : I), C i) = ⋂ (i : I), closure (C i)

Theorem 6.5: Let C i be convex sets in R^n for i ∈ I, and let the sets ri (C i) have a common point. Then cl (⋂ i, C i) = ⋂ i, cl (C i). If I is finite, then also ri (⋂ i, C i) = ⋂ i, ri (C i).

theorem euclideanRelativeInterior_iInter_eq_iInter_relativeInterior_of_finite (n : ℕ) {I : Type u_1} [Finite I] (C : I → Set (EuclideanSpace ℝ (Fin n))) (hC : ∀ (i : I), Convex ℝ (C i)) (hri : (⋂ (i : I), euclideanRelativeInterior n (C i)).Nonempty) : euclideanRelativeInterior n (⋂ (i : I), C i) = ⋂ (i : I), euclideanRelativeInterior n (C i)

Theorem 6.5: If I is finite, then ri (⋂ i, C i) = ⋂ i, ri (C i) under the same assumptions as the preceding statement.

theorem iInter_fin_two_eq_inter {α : Type u_1} (D : Fin 2 → Set α) : ⋂ (i : Fin 2), D i = D 0 ∩ D 1

The intersection of a Fin 2-indexed family is the binary intersection.

theorem ri_iInter_nonempty_from_hM (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (D : Fin 2 → Set (EuclideanSpace ℝ (Fin n))) (hD0 : D 0 = ↑M) (hD1 : D 1 = C) (hM : (↑M ∩ euclideanRelativeInterior n C).Nonempty) : (⋂ (i : Fin 2), euclideanRelativeInterior n (D i)).Nonempty

A point of M ∩ ri C gives a point in the intersection of the relative interiors.

theorem closure_affineSubspace_eq (n : ℕ) (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) : closure ↑M = ↑M

The closure of an affine subspace is itself.

theorem euclideanRelativeInterior_inter_affineSubspace_eq_and_closure_eq (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (hM : (↑M ∩ euclideanRelativeInterior n C).Nonempty) : euclideanRelativeInterior n (↑M ∩ C) = ↑M ∩ euclideanRelativeInterior n C ∧ closure (↑M ∩ C) = ↑M ∩ closure C

Corollary 6.5.1. Let C be convex and let M be an affine set containing a point of ri C. Then ri (M ∩ C) = M ∩ ri C and cl (M ∩ C) = M ∩ cl C.