Theorems · Definition · functional analysis
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.
- Defined in
- Mathlib.Analysis.LocallyConvex.AbsConvex
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- AddCommMonoidstatement and proof · cited by 12,281
- PartialOrderstatement and proof · cited by 6,410
- SeminormedRingstatement and proof · cited by 446
- ClosureOperatorstatement · cited by 371
- AbsConvexproof · cited by 31
- ClosureOperator.ofCompletePredproof · cited by 4
- AbsConvex.sInterproof · cited by 3
Cited by29
Results whose statement or proof uses this declaration.
- subset_absConvexHullstatement and proof · cited by 7
- absConvexHull_minstatement · cited by 4
- absConvex_absConvexHullstatement and proof · cited by 4
- balanced_absConvexHullstatement · cited by 4
- convex_absConvexHullstatement · cited by 3
- absConvexHull_eq_convexHull_balancedHullstatement · cited by 2
- AbsConvex.absConvexHull_eqstatement · cited by 1
- TotallyBounded.absConvexHullstatement · cited by 1
- absConvexHull_emptystatement · cited by 1
- absConvexHull_eq_emptystatement and proof · cited by 1
- absConvexHull_eq_iInterstatement · cited by 1
- absConvexHull_eq_selfstatement and proof · cited by 1