Theorems · Theorem · functional analysis

balancedHull_convexHull_subseteq_absConvexHull

Deprecated since 2026-05-23Use balancedHull_convexHull_subset_absConvexHull instead.

∀ (𝕜 : 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

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

Defined in

Mathlib.Analysis.LocallyConvex.AbsConvex

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldPartialOrderAddCommGroupModule