V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom s))
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom s)) ↔ affineSpan ℝ s = ⊤
refine' ⟨affineSpan_eq_top_of_nonempty_interior, fun h => _⟩
case intro.intro.intro
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom s))
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom s))
obtain ⟨t, hts, b, hb⟩ := AffineBasis.exists_affine_subbasis h
case intro.intro.intro
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom (range ↑b)))
case intro.intro.intro
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom s))
suffices (interior (convexHull ℝ (range b))).Nonempty by
  rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
  refine' this.mono _
  mono*
case intro.intro.intro.intro
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Finset V
hts : ↑t ⊆ s
b : AffineBasis ↑↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom (range ↑b)))
case intro.intro.intro
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom (range ↑b)))
lift t to Finset V using b.finite_set
no goals
case intro.intro.intro.intro
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Finset V
hts : ↑t ⊆ s
b : AffineBasis ↑↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom (range ↑b)))
exact ⟨_, b.centroid_mem_interior_convexHull⟩
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
this : Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom t))
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom s))
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
this : Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom (range ↑b)))
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom s))
rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
this : Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom t))
⊢ interior (↑(convexHull ℝ).toOrderHom t) ⊆ interior (↑(convexHull ℝ).toOrderHom s)
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
this : Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom t))
⊢ Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom s))
refine' this.mono _
no goals
V : Type u_1
P : Type ?u.98022
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
this : Set.Nonempty (interior (↑(convexHull ℝ).toOrderHom t))
⊢ interior (↑(convexHull ℝ).toOrderHom t) ⊆ interior (↑(convexHull ℝ).toOrderHom s)
mono*