Intrinsic frontier and interior

This file defines the intrinsic frontier, interior and closure of a set in a normed additive torsor. These are also known as relative frontier, interior, closure.

The intrinsic frontier/interior/closure of a set s is the frontier/interior/closure of s considered as a set in its affine span.

The intrinsic interior is in general greater than the topological interior, the intrinsic frontier in general less than the topological frontier, and the intrinsic closure in cases of interest the same as the topological closure.

Definitions

• intrinsicInterior: Intrinsic interior
• intrinsicFrontier: Intrinsic frontier
• intrinsicClosure: Intrinsic closure

Results

The main results are:

• AffineIsometry.image_intrinsicInterior/AffineIsometry.image_intrinsicFrontier/ AffineIsometry.image_intrinsicClosure: Intrinsic interiors/frontiers/closures commute with taking the image under an affine isometry.
• Set.Nonempty.intrinsicInterior: The intrinsic interior of a nonempty convex set is nonempty.

References

• Chapter 8 of Barry Simon, Convexity
• Chapter 1 of [Rolf Schneider, Convex Bodies: The Brunn-Minkowski theory][schneider2013].

TODO

• IsClosed s → IsExtreme 𝕜 s (intrinsicFrontier 𝕜 s)
• x ∈ s → y ∈ intrinsicInterior 𝕜 s → openSegment 𝕜 x y ⊆ intrinsicInterior 𝕜 s

def intrinsicInterior (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : Set P

The intrinsic interior of a set is its interior considered as a set in its affine span.

Equations

• intrinsicInterior 𝕜 s = Subtype.val '' interior (Subtype.val ⁻¹' s)

def intrinsicFrontier (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : Set P

The intrinsic frontier of a set is its frontier considered as a set in its affine span.

Equations

• intrinsicFrontier 𝕜 s = Subtype.val '' frontier (Subtype.val ⁻¹' s)

def intrinsicClosure (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : Set P

The intrinsic closure of a set is its closure considered as a set in its affine span.

Equations

• intrinsicClosure 𝕜 s = Subtype.val '' closure (Subtype.val ⁻¹' s)

@[simp]

theorem mem_intrinsicInterior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} {x : P} : x ∈ intrinsicInterior 𝕜 s ↔ ∃ y ∈ interior (Subtype.val ⁻¹' s), ↑y = x

@[simp]

theorem mem_intrinsicFrontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} {x : P} : x ∈ intrinsicFrontier 𝕜 s ↔ ∃ y ∈ frontier (Subtype.val ⁻¹' s), ↑y = x

@[simp]

theorem mem_intrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} {x : P} : x ∈ intrinsicClosure 𝕜 s ↔ ∃ y ∈ closure (Subtype.val ⁻¹' s), ↑y = x

theorem intrinsicInterior_subset {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : intrinsicInterior 𝕜 s ⊆ s

theorem intrinsicFrontier_subset {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} (hs : IsClosed s) : intrinsicFrontier 𝕜 s ⊆ s

theorem intrinsicFrontier_subset_intrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : intrinsicFrontier 𝕜 s ⊆ intrinsicClosure 𝕜 s

theorem subset_intrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : s ⊆ intrinsicClosure 𝕜 s

@[simp]

theorem intrinsicInterior_empty {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] : intrinsicInterior 𝕜 ∅ = ∅

@[simp]

theorem intrinsicFrontier_empty {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] : intrinsicFrontier 𝕜 ∅ = ∅

@[simp]

theorem intrinsicClosure_empty {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] : intrinsicClosure 𝕜 ∅ = ∅

@[simp]

theorem intrinsicClosure_nonempty {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : (intrinsicClosure 𝕜 s).Nonempty ↔ s.Nonempty

theorem Set.Nonempty.intrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : s.Nonempty → (intrinsicClosure 𝕜 s).Nonempty

Alias of the reverse direction of intrinsicClosure_nonempty.

theorem Set.Nonempty.ofIntrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : (intrinsicClosure 𝕜 s).Nonempty → s.Nonempty

Alias of the forward direction of intrinsicClosure_nonempty.

@[simp]

theorem intrinsicInterior_singleton {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (x : P) : intrinsicInterior 𝕜 {x} = {x}

@[simp]

theorem intrinsicFrontier_singleton {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (x : P) : intrinsicFrontier 𝕜 {x} = ∅

@[simp]

theorem intrinsicClosure_singleton {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (x : P) : intrinsicClosure 𝕜 {x} = {x}

Note that neither intrinsicInterior nor intrinsicFrontier is monotone.

theorem intrinsicClosure_mono {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s t : Set P} (h : s ⊆ t) : intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t

theorem interior_subset_intrinsicInterior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : interior s ⊆ intrinsicInterior 𝕜 s

theorem intrinsicClosure_subset_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : intrinsicClosure 𝕜 s ⊆ closure s

theorem intrinsicFrontier_subset_frontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : intrinsicFrontier 𝕜 s ⊆ frontier s

theorem intrinsicClosure_subset_affineSpan {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : intrinsicClosure 𝕜 s ⊆ ↑(affineSpan 𝕜 s)

@[simp]

theorem intrinsicClosure_diff_intrinsicFrontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : intrinsicClosure 𝕜 s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s

@[simp]

theorem intrinsicClosure_diff_intrinsicInterior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : intrinsicClosure 𝕜 s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s

@[simp]

theorem intrinsicInterior_union_intrinsicFrontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s

@[simp]

theorem intrinsicFrontier_union_intrinsicInterior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s

theorem isClosed_intrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} (hs : IsClosed ↑(affineSpan 𝕜 s)) : IsClosed (intrinsicClosure 𝕜 s)

theorem isClosed_intrinsicFrontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} (hs : IsClosed ↑(affineSpan 𝕜 s)) : IsClosed (intrinsicFrontier 𝕜 s)

@[simp]

theorem affineSpan_intrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : affineSpan 𝕜 (intrinsicClosure 𝕜 s) = affineSpan 𝕜 s

theorem IsClosed.intrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} (hs : IsClosed (Subtype.val ⁻¹' s)) : intrinsicClosure 𝕜 s = s

@[simp]

theorem intrinsicClosure_idem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s

@[simp]

theorem AffineIsometry.image_intrinsicInterior {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] [MetricSpace P] [PseudoMetricSpace Q] [NormedAddTorsor V P] [NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) : intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s

@[simp]

theorem AffineIsometry.image_intrinsicFrontier {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] [MetricSpace P] [PseudoMetricSpace Q] [NormedAddTorsor V P] [NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) : intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s

@[simp]

theorem AffineIsometry.image_intrinsicClosure {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] [MetricSpace P] [PseudoMetricSpace Q] [NormedAddTorsor V P] [NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) : intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 s

@[simp]

theorem intrinsicClosure_eq_closure (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] (s : Set P) : intrinsicClosure 𝕜 s = closure s

@[simp]

theorem closure_diff_intrinsicInterior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] (s : Set P) : closure s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s

@[simp]

theorem closure_diff_intrinsicFrontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] (s : Set P) : closure s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s

theorem Set.Nonempty.intrinsicInterior {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {s : Set V} (hscv : Convex ℝ s) (hsne : s.Nonempty) : (intrinsicInterior ℝ s).Nonempty

The intrinsic interior of a nonempty convex set is nonempty.

theorem intrinsicInterior_nonempty {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {s : Set V} (hs : Convex ℝ s) : (intrinsicInterior ℝ s).Nonempty ↔ s.Nonempty