# Convex sets #

In a 𝕜-vector space, we define the following property:

- `Convex 𝕜 s`: A set `s` is convex if for any two points `x y ∈ s` it includes `segment 𝕜 x y`.

We provide various equivalent versions, and prove that some specific sets are convex.

## TODO #

Generalize all this file to affine spaces.

### Convexity of sets #

source
def Convex (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) :
Prop

Convexity of sets.

Equations

- Convex 𝕜 s = ∀ ⦃x : E⦄, x ∈ s → StarConvex 𝕜 x s

Instances For

source
theorem Convex.starConvex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x : E} (hs : Convex 𝕜 s) (hx : x ∈ s) :
StarConvex 𝕜 x s
source
theorem convex_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} :
Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → segment 𝕜 x y ⊆ s
source
theorem Convex.segment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
segment 𝕜 x y ⊆ s
source
theorem Convex.openSegment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
openSegment 𝕜 x y ⊆ s
source
theorem convex_iff_add_mem {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} :
Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
source
theorem convex_iff_pointwise_add_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} :
Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Alternative definition of set convexity, in terms of pointwise set operations.

source
theorem Convex.set_combo_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} :
Convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Alias of the forward direction of `convex_iff_pointwise_add_subset`.

Alternative definition of set convexity, in terms of pointwise set operations.

source
theorem convex_empty {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] :
Convex 𝕜 ∅
source
theorem convex_univ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] :
Convex 𝕜 Set.univ
source
theorem Convex.inter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) :
Convex 𝕜 (s ∩ t)
source
theorem convex_sInter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s) :
Convex 𝕜 (⋂₀ S)
source
theorem convex_iInter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E} (h : ∀ (i : ι), Convex 𝕜 (s i)) :
Convex 𝕜 (⋂ (i : ι), s i)
source
theorem convex_iInter₂ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {κ : ι → Sort u_6} {s : (i : ι) → κ i → Set E} (h : ∀ (i : ι) (j : κ i), Convex 𝕜 (s i j)) :
Convex 𝕜 (⋂ (i : ι), ⋂ (j : κ i), s i j)
source
theorem Convex.prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [SMul 𝕜 E] [SMul 𝕜 F] {s : Set E} {t : Set F} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) :
Convex 𝕜 (s ×ˢ t)
source
theorem convex_pi {𝕜 : Type u_1} [Semiring 𝕜] [PartialOrder 𝕜] {ι : Type u_5} {E : ι → Type u_6} [(i : ι) → AddCommMonoid (E i)] [(i : ι) → SMul 𝕜 (E i)] {s : Set ι} {t : (i : ι) → Set (E i)} (ht : ∀ ⦃i : ι⦄, i ∈ s → Convex 𝕜 (t i)) :
Convex 𝕜 (s.pi t)
source
theorem Directed.convex_iUnion {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E} (hdir : Directed (fun (x1 x2 : Set E) => x1 ⊆ x2) s) (hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)) :
Convex 𝕜 (⋃ (i : ι), s i)
source
theorem DirectedOn.convex_sUnion {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {c : Set (Set E)} (hdir : DirectedOn (fun (x1 x2 : Set E) => x1 ⊆ x2) c) (hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A) :
Convex 𝕜 (⋃₀ c)
source
theorem convex_iff_openSegment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [ZeroLEOneClass 𝕜] :
Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s
source
theorem convex_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
source
theorem convex_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
Convex 𝕜 s ↔ s.Pairwise fun (x y : E) => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
source
theorem Convex.starConvex_iff {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} [ZeroLEOneClass 𝕜] (hs : Convex 𝕜 s) (h : s.Nonempty) :
StarConvex 𝕜 x s ↔ x ∈ s
source
theorem Set.Subsingleton.convex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (h : s.Subsingleton) :
Convex 𝕜 s
source
@[simp]
theorem convex_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (c : E) :
Convex 𝕜 {c}
source
theorem convex_zero {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
Convex 𝕜 0
source
theorem convex_segment {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [IsOrderedRing 𝕜] (x y : E) :
Convex 𝕜 (segment 𝕜 x y)
source
theorem Convex.linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set E} (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) :
Convex 𝕜 (⇑f '' s)

See `Convex.semilinear_image` for a version for semilinar maps, but requiring that `𝕜` be a linear order, instead of just a partial order.

source
theorem Convex.is_linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set E} (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) :
Convex 𝕜 (f '' s)
source
theorem Convex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) :
Convex 𝕜 (⇑f ⁻¹' s)
source
theorem Convex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) :
Convex 𝕜 (f ⁻¹' s)
source
theorem Convex.add {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) :
Convex 𝕜 (s + t)
source
noncomputable def convexAddSubmonoid (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
AddSubmonoid (Set E)

The convex sets form an additive submonoid under pointwise addition.

Equations

- convexAddSubmonoid 𝕜 E = { carrier := {s : Set E | Convex 𝕜 s}, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source
@[simp]
theorem coe_convexAddSubmonoid (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
↑(convexAddSubmonoid 𝕜 E) = {s : Set E | Convex 𝕜 s}
source
@[simp]
theorem mem_convexAddSubmonoid {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
s ∈ convexAddSubmonoid 𝕜 E ↔ Convex 𝕜 s
source
theorem convex_list_sum {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {l : List (Set E)} (h : ∀ i ∈ l, Convex 𝕜 i) :
Convex 𝕜 l.sum
source
theorem convex_multiset_sum {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Multiset (Set E)} (h : ∀ i ∈ s, Convex 𝕜 i) :
Convex 𝕜 s.sum
source
theorem convex_sum {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ι : Type u_5} {s : Finset ι} (t : ι → Set E) (h : ∀ i ∈ s, Convex 𝕜 (t i)) :
Convex 𝕜 (∑ i ∈ s, t i)
source
theorem Convex.vadd {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) :
Convex 𝕜 (z +ᵥ s)
source
theorem Convex.translate {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) :
Convex 𝕜 ((fun (x : E) => z + x) '' s)
source
theorem Convex.translate_preimage_right {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) :
Convex 𝕜 ((fun (x : E) => z + x) ⁻¹' s)

The translation of a convex set is also convex.

source
theorem Convex.translate_preimage_left {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) :
Convex 𝕜 ((fun (x : E) => x + z) ⁻¹' s)

The translation of a convex set is also convex.

source
theorem convex_Iic {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r : β) :
Convex 𝕜 (Set.Iic r)
source
theorem convex_Ici {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r : β) :
Convex 𝕜 (Set.Ici r)
source
theorem convex_Icc {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r s : β) :
Convex 𝕜 (Set.Icc r s)
source
theorem convex_halfSpace_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) :
Convex 𝕜 {w : E | f w ≤ r}
source
theorem convex_halfSpace_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) :
Convex 𝕜 {w : E | r ≤ f w}
source
theorem convex_hyperplane {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) :
Convex 𝕜 {w : E | f w = r}
source
theorem convex_Iio {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β) :
Convex 𝕜 (Set.Iio r)
source
theorem convex_Ioi {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β) :
Convex 𝕜 (Set.Ioi r)
source
theorem convex_Ioo {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β) :
Convex 𝕜 (Set.Ioo r s)
source
theorem convex_Ico {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β) :
Convex 𝕜 (Set.Ico r s)
source
theorem convex_Ioc {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β) :
Convex 𝕜 (Set.Ioc r s)
source
theorem convex_halfSpace_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) :
Convex 𝕜 {w : E | f w < r}
source
theorem convex_halfSpace_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) :
Convex 𝕜 {w : E | r < f w}
source
theorem convex_uIcc {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r s : β) :
Convex 𝕜 (Set.uIcc r s)
source
theorem Convex.lift {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [Module 𝕜 E] (R : Type u_5) [Semiring R] [PartialOrder R] [Module R E] [Module R 𝕜] [IsScalarTower R 𝕜 E] [SMulPosMono R 𝕜] {s : Set E} (hs : Convex 𝕜 s) :
Convex R s

Lift the convexity of a set up through a scalar tower.

source
theorem MonotoneOn.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) :
Convex 𝕜 {x : E | x ∈ s ∧ f x ≤ r}
source
theorem MonotoneOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) :
Convex 𝕜 {x : E | x ∈ s ∧ f x < r}
source
theorem MonotoneOn.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) :
Convex 𝕜 {x : E | x ∈ s ∧ r ≤ f x}
source
theorem MonotoneOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) :
Convex 𝕜 {x : E | x ∈ s ∧ r < f x}
source
theorem AntitoneOn.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) :
Convex 𝕜 {x : E | x ∈ s ∧ f x ≤ r}
source
theorem AntitoneOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) :
Convex 𝕜 {x : E | x ∈ s ∧ f x < r}
source
theorem AntitoneOn.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) :
Convex 𝕜 {x : E | x ∈ s ∧ r ≤ f x}
source
theorem AntitoneOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) :
Convex 𝕜 {x : E | x ∈ s ∧ r < f x}
source
theorem Monotone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Monotone f) (r : β) :
Convex 𝕜 {x : E | f x ≤ r}
source
theorem Monotone.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Monotone f) (r : β) :
Convex 𝕜 {x : E | f x ≤ r}
source
theorem Monotone.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Monotone f) (r : β) :
Convex 𝕜 {x : E | r ≤ f x}
source
theorem Monotone.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Monotone f) (r : β) :
Convex 𝕜 {x : E | f x ≤ r}
source
theorem Antitone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) :
Convex 𝕜 {x : E | f x ≤ r}
source
theorem Antitone.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) :
Convex 𝕜 {x : E | f x < r}
source
theorem Antitone.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) :
Convex 𝕜 {x : E | r ≤ f x}
source
theorem Antitone.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) :
Convex 𝕜 {x : E | r < f x}
source
theorem Convex.smul {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (c : 𝕜) :
Convex 𝕜 (c • s)
source
theorem Convex.smul_preimage {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (c : 𝕜) :
Convex 𝕜 ((fun (z : E) => c • z) ⁻¹' s)
source
theorem Convex.affinity {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) (c : 𝕜) :
Convex 𝕜 ((fun (x : E) => z + c • x) '' s)
source
theorem convex_openSegment {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b : E) :
Convex 𝕜 (openSegment 𝕜 a b)
source
@[simp]
theorem convex_vadd {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (a : E) :
Convex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s
source
theorem AffineSubspace.convex {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (Q : AffineSubspace 𝕜 E) :
Convex 𝕜 ↑Q

Affine subspaces are convex.

source
theorem Convex.affine_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) {s : Set F} (hs : Convex 𝕜 s) :
Convex 𝕜 (⇑f ⁻¹' s)

The preimage of a convex set under an affine map is convex.

source
theorem Convex.affine_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] {s : Set E} (f : E →ᵃ[𝕜] F) (hs : Convex 𝕜 s) :
Convex 𝕜 (⇑f '' s)

The image of a convex set under an affine map is convex.

source
theorem Convex.neg {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) :
Convex 𝕜 (-s)
source
theorem Convex.sub {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) :
Convex 𝕜 (s - t)
source
theorem Convex.add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) :
x + t • y ∈ s
source
theorem Convex.smul_mem_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (hs : Convex 𝕜 s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) :
t • x ∈ s
source
theorem Convex.mapsTo_lineMap {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
Set.MapsTo (⇑(AffineMap.lineMap x y)) (Set.Icc 0 1) s
source
theorem Convex.lineMap_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) :
(AffineMap.lineMap x y) t ∈ s
source
theorem Convex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) :
x + t • (y - x) ∈ s
source
theorem Convex.semilinear_image {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommMonoid E] [PartialOrder 𝕜] {𝕜' : Type u_5} [Semiring 𝕜'] [PartialOrder 𝕜'] {σ : 𝕜 →+* 𝕜'} [RingHomSurjective σ] {F' : Type u_6} [AddCommMonoid F'] [Module 𝕜' F'] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (hσ : ∀ {s t : 𝕜}, σ s ≤ σ t ↔ s ≤ t) (f : E →ₛₗ[σ] F') :
Convex 𝕜' (⇑f '' s)
source
theorem Convex_subadditive_le {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommMonoid E] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y) (hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x) (B : 𝕜) :
Convex 𝕜 {x : E | f x ≤ B}
source
theorem Convex.midpoint_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] {s : Set E} {x y : E} (h : Convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) :
midpoint 𝕜 x y ∈ s
source
theorem convex_iff_div {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} :
Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Alternative definition of set convexity, using division.

source
theorem Convex.mem_smul_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
x ∈ t • s
source
theorem Convex.exists_mem_add_smul_eq {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x y : E} {p q : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (hp : 0 ≤ p) (hq : 0 ≤ q) :
∃ z ∈ s, (p + q) • z = p • x + q • y
source
theorem Convex.add_smul {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) :
(p + q) • s = p • s + q • s

#### Convex sets in an ordered space #

Relates `Convex` and `OrdConnected`.

source
theorem Set.OrdConnected.convex_of_chain {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} (hs : s.OrdConnected) (h : IsChain (fun (x1 x2 : E) => x1 ≤ x2) s) :
Convex 𝕜 s
source
theorem Set.OrdConnected.convex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} (hs : s.OrdConnected) :
Convex 𝕜 s
source
theorem convex_iff_ordConnected {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} :
Convex 𝕜 s ↔ s.OrdConnected
source
theorem Convex.ordConnected {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} :
Convex 𝕜 s → s.OrdConnected

Alias of the forward direction of `convex_iff_ordConnected`.

#### Convexity of submodules/subspaces #

source
theorem Submodule.convex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (K : Submodule 𝕜 E) :
Convex 𝕜 ↑K
source
theorem Submodule.starConvex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (K : Submodule 𝕜 E) :
StarConvex 𝕜 0 ↑K
source
theorem Submodule.Convex.semilinear_range {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {𝕜' : Type u_5} [Semiring 𝕜'] {σ : 𝕜' →+* 𝕜} [RingHomSurjective σ] {F' : Type u_6} [AddCommMonoid F'] [Module 𝕜' F'] (f : F' →ₛₗ[σ] E) :
Convex 𝕜 ↑(LinearMap.range f)
source
theorem convex_of_nonneg_surjective_algebraMap {R : Type u_5} [CommSemiring R] (A : Type u_6) [Semiring A] [Algebra R A] {M : Type u_7} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [PartialOrder R] [PartialOrder A] [FaithfulSMul R A] {s : Set M} (halg : Set.Ici 0 ⊆ ⇑(algebraMap R A) '' Set.Ici 0) (hs : Convex R s) :
Convex A s