Absolutely convex sets

A set s in an commutative monoid E is called absolutely convex or disked if it is convex and balanced. The importance of absolutely convex sets comes from the fact that every locally convex topological vector space has a basis consisting of absolutely convex sets.

Main definitions

• absConvexHull: the absolutely convex hull of a set s is the smallest absolutely convex set containing s;
• closedAbsConvexHull: the closed absolutely convex hull of a set s is the smallest absolutely convex set containing s;

Main statements

• absConvexHull_eq_convexHull_balancedHull: when the locally convex space is a module, the absolutely convex hull of a set s equals the convex hull of the balanced hull of s;
• convexHull_union_neg_eq_absConvexHull: the convex hull of s ∪ -s is the absolutely convex hull of s;
• closedAbsConvexHull_closure_eq_closedAbsConvexHull : the closed absolutely convex hull of the closure of s equals the closed absolutely convex hull of s;

Tags

disks, convex, balanced

def AbsConvex (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] (s : Set E) : Prop

A set is absolutely convex if it is balanced and convex.

Equations

• AbsConvex 𝕜 s = (Balanced 𝕜 s ∧ Convex 𝕜 s)

theorem AbsConvex.empty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] : AbsConvex 𝕜 ∅

theorem AbsConvex.univ {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] : AbsConvex 𝕜 Set.univ

theorem AbsConvex.inter {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s t : Set E} (hs : AbsConvex 𝕜 s) (ht : AbsConvex 𝕜 t) : AbsConvex 𝕜 (s ∩ t)

theorem AbsConvex.sInter {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {S : Set (Set E)} (h : ∀ s ∈ S, AbsConvex 𝕜 s) : AbsConvex 𝕜 (⋂₀ S)

theorem AbsConvex.iInter {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {ι : Sort u_3} {s : ι → Set E} (h : ∀ (i : ι), AbsConvex 𝕜 (s i)) : AbsConvex 𝕜 (⋂ (i : ι), s i)

theorem AbsConvex.iInter₂ {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {ι : Sort u_3} {κ : ι → Sort u_4} {f : (i : ι) → κ i → Set E} (h : ∀ (i : ι) (j : κ i), AbsConvex 𝕜 (f i j)) : AbsConvex 𝕜 (⋂ (i : ι), ⋂ (j : κ i), f i j)

def absConvexHull (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] : ClosureOperator (Set E)

The absolute convex hull of a set s is the minimal absolute convex set that includes s.

Equations

• absConvexHull 𝕜 = ClosureOperator.ofCompletePred (AbsConvex 𝕜) ⋯

@[simp]

theorem absConvexHull_isClosed (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] (s : Set E) : (absConvexHull 𝕜).IsClosed s = AbsConvex 𝕜 s

theorem subset_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : s ⊆ (absConvexHull 𝕜) s

theorem absConvex_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : AbsConvex 𝕜 ((absConvexHull 𝕜) s)

theorem balanced_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : Balanced 𝕜 ((absConvexHull 𝕜) s)

theorem convex_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : Convex 𝕜 ((absConvexHull 𝕜) s)

theorem absConvexHull_eq_iInter (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] (s : Set E) : (absConvexHull 𝕜) s = ⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t

theorem mem_absConvexHull_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} {x : E} : x ∈ (absConvexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t

theorem absConvexHull_min {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s t : Set E} : s ⊆ t → AbsConvex 𝕜 t → (absConvexHull 𝕜) s ⊆ t

theorem AbsConvex.absConvexHull_subset_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s t : Set E} (ht : AbsConvex 𝕜 t) : (absConvexHull 𝕜) s ⊆ t ↔ s ⊆ t

theorem absConvexHull_mono {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s t : Set E} (hst : s ⊆ t) : (absConvexHull 𝕜) s ⊆ (absConvexHull 𝕜) t

theorem absConvexHull_eq_self {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : (absConvexHull 𝕜) s = s ↔ AbsConvex 𝕜 s

theorem AbsConvex.absConvexHull_eq {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : AbsConvex 𝕜 s → (absConvexHull 𝕜) s = s

Alias of the reverse direction of absConvexHull_eq_self.

@[simp]

theorem absConvexHull_univ {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] : (absConvexHull 𝕜) Set.univ = Set.univ

@[simp]

theorem absConvexHull_empty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] : (absConvexHull 𝕜) ∅ = ∅

@[simp]

theorem absConvexHull_eq_empty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : (absConvexHull 𝕜) s = ∅ ↔ s = ∅

@[simp]

theorem absConvexHull_nonempty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty

theorem Set.Nonempty.absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] {s : Set E} : s.Nonempty → ((absConvexHull 𝕜) s).Nonempty

Alias of the reverse direction of absConvexHull_nonempty.

theorem absConvex_closed_sInter {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] {S : Set (Set E)} (h : ∀ s ∈ S, AbsConvex 𝕜 s ∧ IsClosed s) : AbsConvex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S)

def closedAbsConvexHull (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] : ClosureOperator (Set E)

The absolutely convex closed hull of a set s is the minimal absolutely convex closed set that includes s.

Equations

• closedAbsConvexHull 𝕜 = ClosureOperator.ofCompletePred (fun (s : Set E) => AbsConvex 𝕜 s ∧ IsClosed s) ⋯

@[simp]

theorem closedAbsConvexHull_isClosed (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] (s : Set E) : (closedAbsConvexHull 𝕜).IsClosed s = (AbsConvex 𝕜 s ∧ IsClosed s)

theorem absConvex_convexClosedHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] {s : Set E} : AbsConvex 𝕜 ((closedAbsConvexHull 𝕜) s)

theorem isClosed_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] {s : Set E} : IsClosed ((closedAbsConvexHull 𝕜) s)

theorem subset_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] {s : Set E} : s ⊆ (closedAbsConvexHull 𝕜) s

theorem closure_subset_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] {s : Set E} : closure s ⊆ (closedAbsConvexHull 𝕜) s

theorem closedAbsConvexHull_min {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] {s t : Set E} (hst : s ⊆ t) (h_conv : AbsConvex 𝕜 t) (h_closed : IsClosed t) : (closedAbsConvexHull 𝕜) s ⊆ t

theorem absConvexHull_subset_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] {s : Set E} : (absConvexHull 𝕜) s ⊆ (closedAbsConvexHull 𝕜) s

@[simp]

theorem closedAbsConvexHull_closure_eq_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [PartialOrder 𝕜] [TopologicalSpace E] {s : Set E} : (closedAbsConvexHull 𝕜) (closure s) = (closedAbsConvexHull 𝕜) s

theorem AbsConvex.closure {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : AbsConvex 𝕜 s) : AbsConvex 𝕜 (_root_.closure s)

theorem closedAbsConvexHull_eq_closure_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E} : (closedAbsConvexHull 𝕜) s = closure ((absConvexHull 𝕜) s)

theorem nhds_hasBasis_absConvex (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [ContinuousSMul 𝕜 E] : (nhds 0).HasBasis (fun (s : Set E) => s ∈ nhds 0 ∧ AbsConvex 𝕜 s) id

theorem nhds_hasBasis_absConvex_open (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [ContinuousSMul 𝕜 E] [IsTopologicalAddGroup E] [ZeroLEOneClass 𝕜] : (nhds 0).HasBasis (fun (s : Set E) => 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s) id

theorem absConvexHull_add_subset (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} : (absConvexHull 𝕜) (s + t) ⊆ (absConvexHull 𝕜) s + (absConvexHull 𝕜) t

theorem absConvexHull_eq_convexHull_balancedHull (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : (absConvexHull 𝕜) s = (convexHull 𝕜) (balancedHull 𝕜 s)

theorem balancedHull_convexHull_subseteq_absConvexHull (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : balancedHull 𝕜 ((convexHull 𝕜) s) ⊆ (absConvexHull 𝕜) s

In general, equality doesn't hold here - e.g. consider s := {(-1, 1), (1, 1)} in ℝ².

theorem balancedHull_subset_convexHull_union_neg {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} : balancedHull ℝ s ⊆ (convexHull ℝ) (s ∪ -s)

@[simp]

theorem convexHull_union_neg_eq_absConvexHull {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} : (convexHull ℝ) (s ∪ -s) = (absConvexHull ℝ) s

theorem totallyBounded_absConvexHull (E : Type u_2) [AddCommGroup E] [Module ℝ E] {s : Set E} [UniformSpace E] [IsUniformAddGroup E] [lcs : LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E] (hs : TotallyBounded s) : TotallyBounded ((absConvexHull ℝ) s)

theorem zero_mem_absConvexHull {𝕜 : Type u_1} {E : Type u_2} {s : Set E} [SeminormedRing 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nonempty ↑s] : 0 ∈ (absConvexHull 𝕜) s

theorem isCompact_closedAbsConvexHull_of_totallyBounded {E : Type u_3} [AddCommGroup E] [Module ℝ E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [QuasiCompleteSpace ℝ E] {s : Set E} (ht : TotallyBounded s) : IsCompact ((closedAbsConvexHull ℝ) s)

Bourbaki, Topological Vector Spaces, III §1.6