Theorems · Theorem · functional analysis

balancedHull_convexHull_subset_absConvexHull

∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : 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 ℝ².

Defined in

Mathlib.Analysis.LocallyConvex.AbsConvex

Cited by

1 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldPartialOrderAddCommGroupModule