[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ x ∈ ↑(convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
[PROOFSTEP]
simp_rw [convexHull_eq_iInter, mem_iInter]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ ↑(convexHull 𝕜) s = ∅ ↔ s = ∅
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ ↑(convexHull 𝕜) s = ∅ → s = ∅
[PROOFSTEP]
intro h
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
h : ↑(convexHull 𝕜) s = ∅
⊢ s = ∅
[PROOFSTEP]
rw [← Set.subset_empty_iff, ← h]
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
h : ↑(convexHull 𝕜) s = ∅
⊢ s ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
exact subset_convexHull 𝕜 _
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ s = ∅ → ↑(convexHull 𝕜) s = ∅
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
t : Set E
x y : E
⊢ ↑(convexHull 𝕜) ∅ = ∅
[PROOFSTEP]
exact convexHull_empty
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ Set.Nonempty (↑(convexHull 𝕜) s) ↔ Set.Nonempty s
[PROOFSTEP]
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne.def, Ne.def]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ ¬↑(convexHull 𝕜) s = ∅ ↔ ¬s = ∅
[PROOFSTEP]
exact not_congr convexHull_empty_iff
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ x y : E
⊢ ↑(convexHull 𝕜) {x, y} = segment 𝕜 x y
[PROOFSTEP]
refine
  (convexHull_min ?_ <| convex_segment _ _).antisymm
    (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ x y : E
⊢ {x, y} ⊆ segment 𝕜 x y
[PROOFSTEP]
rw [insert_subset_iff, singleton_subset_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
[PROOFSTEP]
exact ⟨left_mem_segment _ _ _, right_mem_segment _ _ _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ Convex 𝕜 (s \ {x}) ↔ ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ Convex 𝕜 (s \ {x}) → ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
[PROOFSTEP]
rintro hsx hx
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : x ∈ ↑(convexHull 𝕜) (s \ {x})
⊢ False
[PROOFSTEP]
rw [hsx.convexHull_eq] at hx 
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : x ∈ s \ {x}
⊢ False
[PROOFSTEP]
exact hx.2 (mem_singleton _)
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ ¬x ∈ ↑(convexHull 𝕜) (s \ {x}) → Convex 𝕜 (s \ {x})
[PROOFSTEP]
rintro hx
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
hx : ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
⊢ Convex 𝕜 (s \ {x})
[PROOFSTEP]
suffices h : s \ { x } = convexHull 𝕜 (s \ { x })
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
hx : ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
h : s \ {x} = ↑(convexHull 𝕜) (s \ {x})
⊢ Convex 𝕜 (s \ {x})
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
hx : ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
h : s \ {x} = ↑(convexHull 𝕜) (s \ {x})
⊢ Convex 𝕜 (↑(convexHull 𝕜) (s \ {x}))
[PROOFSTEP]
exact convex_convexHull 𝕜 _
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y : E
s : Set E
hs : Convex 𝕜 s
x : E
hx : ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
⊢ s \ {x} = ↑(convexHull 𝕜) (s \ {x})
[PROOFSTEP]
exact
  Subset.antisymm (subset_convexHull 𝕜 _) fun y hy =>
    ⟨convexHull_min (diff_subset _ _) hs hy, by
      rintro (rfl : y = x)
      exact hx hy⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y✝ : E
s : Set E
hs : Convex 𝕜 s
x : E
hx : ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
y : E
hy : y ∈ ↑(convexHull 𝕜) (s \ {x})
⊢ ¬y ∈ {x}
[PROOFSTEP]
rintro (rfl : y = x)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x y✝ : E
s : Set E
hs : Convex 𝕜 s
y : E
hx : ¬y ∈ ↑(convexHull 𝕜) (s \ {y})
hy : y ∈ ↑(convexHull 𝕜) (s \ {y})
⊢ False
[PROOFSTEP]
exact hx hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑f '' ↑(convexHull 𝕜) s = ↑(convexHull 𝕜) (↑f '' s)
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑f '' ↑(convexHull 𝕜) s ⊆ ↑(convexHull 𝕜) (↑f '' s)
[PROOFSTEP]
rw [Set.image_subset_iff]
[GOAL]
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑(convexHull 𝕜) s ⊆ ↑f ⁻¹' ↑(convexHull 𝕜) (↑f '' s)
[PROOFSTEP]
refine' convexHull_min _ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)
[GOAL]
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ s ⊆ ↑f ⁻¹' ↑(convexHull 𝕜) (↑f '' s)
[PROOFSTEP]
rw [← Set.image_subset_iff]
[GOAL]
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑f '' s ⊆ ↑(convexHull 𝕜) (↑f '' s)
[PROOFSTEP]
exact subset_convexHull 𝕜 (f '' s)
[GOAL]
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑(convexHull 𝕜) (↑f '' s) ⊆ ↑f '' ↑(convexHull 𝕜) s
[PROOFSTEP]
exact convexHull_min (Set.image_subset _ (subset_convexHull 𝕜 s)) ((convex_convexHull 𝕜 s).affine_image f)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
⊢ affineSpan 𝕜 (↑(convexHull 𝕜) s) = affineSpan 𝕜 s
[PROOFSTEP]
refine' le_antisymm _ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
⊢ affineSpan 𝕜 (↑(convexHull 𝕜) s) ≤ affineSpan 𝕜 s
[PROOFSTEP]
rw [affineSpan_le]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
⊢ ↑(convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)
[PROOFSTEP]
exact convexHull_subset_affineSpan s
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ s : Set E
⊢ ↑(convexHull 𝕜) (-s) = -↑(convexHull 𝕜) s
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ s : Set E
⊢ ↑(convexHull 𝕜) (Neg.neg '' s) = Neg.neg '' ↑(convexHull 𝕜) s
[PROOFSTEP]
exact (AffineMap.image_convexHull _ <| -1).symm
