Documentation

Mathlib.Analysis.Convex.Intrinsic

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 #

Results #

The main results are:

References #

TODO #

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
Instances For
    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
    Instances For
      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
      Instances For
        @[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} :
        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) :
        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} :
        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} :
        @[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] :
        @[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] :
        @[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] :
        @[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} :
        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} :

        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} :

        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) :
        @[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 : Set P} {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} :
        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} :
        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} :
        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)) :
        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)) :
        @[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

        The intrinsic interior of a nonempty convex set is nonempty.