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 sets
is the smallest absolutely convex set containings
;closedAbsConvexHull
: the closed absolutely convex hull of a sets
is the smallest absolutely convex set containings
;
Main statements #
absConvexHull_eq_convexHull_balancedHull
: when the locally convex space is a module, the absolutely convex hull of a sets
equals the convex hull of the balanced hull ofs
;convexHull_union_neg_eq_absConvexHull
: the convex hull ofs βͺ -s
is the absolutely convex hull ofs
;closedAbsConvexHull_closure_eq_closedAbsConvexHull
: the closed absolutely convex hull of the closure ofs
equals the closed absolutely convex hull ofs
;
Tags #
disks, convex, balanced
def
AbsConvex
(π : Type u_1)
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
(s : Set E)
:
A set is absolutely convex if it is balanced and convex.
Instances For
theorem
AbsConvex.empty
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
:
theorem
AbsConvex.univ
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
:
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)
:
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)
:
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 π) β―
Instances For
@[simp]
theorem
absConvexHull_isClosed
(π : Type u_1)
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
(s : Set E)
:
theorem
subset_absConvexHull
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
{s : Set E}
:
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)
:
theorem
mem_absConvexHull_iff
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
{s : Set E}
{x : E}
:
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)
:
theorem
absConvexHull_mono
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
{s t : Set E}
(hst : s β t)
:
theorem
absConvexHull_eq_self
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
{s : Set E}
:
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 π]
:
@[simp]
theorem
absConvexHull_empty
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
:
@[simp]
theorem
absConvexHull_eq_empty
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
{s : Set E}
:
@[simp]
theorem
absConvexHull_nonempty
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
{s : Set E}
:
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)
:
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) β―
Instances For
@[simp]
theorem
closedAbsConvexHull_isClosed
(π : Type u_1)
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
[TopologicalSpace E]
(s : Set E)
:
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}
:
theorem
closure_subset_closedAbsConvexHull
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
[TopologicalSpace E]
{s : Set E}
:
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)
:
theorem
absConvexHull_subset_closedAbsConvexHull
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
[TopologicalSpace E]
{s : Set E}
:
@[simp]
theorem
closedAbsConvexHull_closure_eq_closedAbsConvexHull
{π : Type u_1}
{E : Type u_2}
[SeminormedRing π]
[SMul π E]
[AddCommMonoid E]
[PartialOrder π]
[TopologicalSpace E]
{s : Set E}
:
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}
:
theorem
nhds_hasBasis_absConvex
(π : Type u_1)
(E : Type u_2)
[NontriviallyNormedField π]
[PartialOrder π]
[AddCommGroup E]
[Module π E]
[TopologicalSpace E]
[LocallyConvexSpace π E]
[ContinuousSMul π E]
:
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 π]
:
theorem
absConvexHull_add_subset
(π : Type u_1)
{E : Type u_2}
[NontriviallyNormedField π]
[PartialOrder π]
[AddCommGroup E]
[Module π E]
{s t : Set E}
:
theorem
absConvexHull_eq_convexHull_balancedHull
(π : Type u_1)
{E : Type u_2}
[NontriviallyNormedField π]
[PartialOrder π]
[AddCommGroup E]
[Module π E]
{s : Set E}
:
theorem
balancedHull_convexHull_subseteq_absConvexHull
(π : Type u_1)
{E : Type u_2}
[NontriviallyNormedField π]
[PartialOrder π]
[AddCommGroup E]
[Module π E]
{s : Set E}
:
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}
:
@[simp]
theorem
convexHull_union_neg_eq_absConvexHull
{E : Type u_2}
[AddCommGroup E]
[Module β E]
{s : Set E}
:
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]
:
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)