[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
cases' ne_or_eq (affineSpan ℝ s) ⊤ with hspan hspan
[GOAL]
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
refine' measure_mono_null _ (addHaar_affineSubspace _ _ hspan)
[GOAL]
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ frontier s ⊆ ↑(affineSpan ℝ s)
[PROOFSTEP]
exact
  frontier_subset_closure.trans (closure_minimal (subset_affineSpan _ _) (affineSpan ℝ s).closed_of_finiteDimensional)
[GOAL]
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s = ⊤
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
rw [← hs.interior_nonempty_iff_affineSpan_eq_top] at hspan
[GOAL]
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : Set.Nonempty (interior s)
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
rcases hspan with
  ⟨x, hx⟩
    /- Without loss of generality, `s` is bounded. Indeed, `∂s ⊆ ⋃ n, ∂(s ∩ ball x (n + 1))`, hence it
        suffices to prove that `∀ n, μ (s ∩ ball x (n + 1)) = 0`; the latter set is bounded.
        -/
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
suffices H : ∀ t : Set E, Convex ℝ t → x ∈ interior t → Bounded t → μ (frontier t) = 0
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
let B : ℕ → Set E := fun n => ball x (n + 1)
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
have : μ (⋃ n : ℕ, frontier (s ∩ B n)) = 0 :=
  by
  refine' measure_iUnion_null fun n => H _ (hs.inter (convex_ball _ _)) _ (bounded_ball.mono (inter_subset_right _ _))
  rw [interior_inter, isOpen_ball.interior_eq]
  exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
⊢ ↑↑μ (⋃ (n : ℕ), frontier (s ∩ B n)) = 0
[PROOFSTEP]
refine' measure_iUnion_null fun n => H _ (hs.inter (convex_ball _ _)) _ (bounded_ball.mono (inter_subset_right _ _))
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
n : ℕ
⊢ x ∈ interior (s ∩ B n)
[PROOFSTEP]
rw [interior_inter, isOpen_ball.interior_eq]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
n : ℕ
⊢ x ∈ interior s ∩ ball x (↑n + 1)
[PROOFSTEP]
exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
this : ↑↑μ (⋃ (n : ℕ), frontier (s ∩ B n)) = 0
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
refine' measure_mono_null (fun y hy => _) this
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
this : ↑↑μ (⋃ (n : ℕ), frontier (s ∩ B n)) = 0
y : E
hy : y ∈ frontier s
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
[PROOFSTEP]
clear this
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
[PROOFSTEP]
set N : ℕ := ⌊dist y x⌋₊
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
[PROOFSTEP]
refine' mem_iUnion.2 ⟨N, _⟩
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ frontier (s ∩ B N)
[PROOFSTEP]
have hN : y ∈ B N := by simp [Nat.lt_floor_add_one]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ B N
[PROOFSTEP]
simp [Nat.lt_floor_add_one]
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N)
[PROOFSTEP]
suffices : y ∈ frontier (s ∩ B N) ∩ B N
[GOAL]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
this : y ∈ frontier (s ∩ B N) ∩ B N
⊢ y ∈ frontier (s ∩ B N)
case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N) ∩ B N
[PROOFSTEP]
exact this.1
[GOAL]
case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N) ∩ B N
[PROOFSTEP]
rw [frontier_inter_open_inter isOpen_ball]
[GOAL]
case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier s ∩ ball x (↑N + 1)
[PROOFSTEP]
exact ⟨hy, hN⟩
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
⊢ ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
[PROOFSTEP]
intro s hs hx hb
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Metric.Bounded s
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
replace hb : μ (interior s) ≠ ∞
[GOAL]
case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Metric.Bounded s
⊢ ↑↑μ (interior s) ≠ ⊤
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
exact (hb.mono interior_subset).measure_lt_top.ne
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
suffices μ (closure s) ≤ μ (interior s) by
  rwa [frontier, measure_diff interior_subset_closure isOpen_interior.measurableSet hb, tsub_eq_zero_iff_le]
    /- Due to `Convex.closure_subset_image_homothety_interior_of_one_lt`, for any `r > 1` we have
        `closure s ⊆ homothety x r '' interior s`, hence `μ (closure s) ≤ r ^ d * μ (interior s)`,
        where `d = finrank ℝ E`. -/
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
this : ↑↑μ (closure s) ≤ ↑↑μ (interior s)
⊢ ↑↑μ (frontier s) = 0
[PROOFSTEP]
rwa [frontier, measure_diff interior_subset_closure isOpen_interior.measurableSet hb, tsub_eq_zero_iff_le]
  /- Due to `Convex.closure_subset_image_homothety_interior_of_one_lt`, for any `r > 1` we have
      `closure s ⊆ homothety x r '' interior s`, hence `μ (closure s) ≤ r ^ d * μ (interior s)`,
      where `d = finrank ℝ E`. -/
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
[PROOFSTEP]
set d : ℕ := FiniteDimensional.finrank ℝ E
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
[PROOFSTEP]
have : ∀ r : ℝ≥0, 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s) :=
  by
  intro r hr
  refine' (measure_mono <| hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq _
  rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
⊢ ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
[PROOFSTEP]
intro r hr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
[PROOFSTEP]
refine' (measure_mono <| hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq _
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ ↑↑μ (↑(AffineMap.homothety x ↑r) '' interior s) = ↑(r ^ d) * ↑↑μ (interior s)
[PROOFSTEP]
rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
[PROOFSTEP]
have : ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure s) ≤ ↑(r ^ d) * μ (interior s) := mem_of_superset self_mem_nhdsWithin this
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
[PROOFSTEP]
refine' ge_of_tendsto _ this
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ Tendsto (fun c => ↑(c ^ d) * ↑↑μ (interior s)) (𝓝[Ioi 1] 1) (𝓝 (↑↑μ (interior s)))
[PROOFSTEP]
refine'
  (((ENNReal.continuous_mul_const hb).comp (ENNReal.continuous_coe.comp (continuous_pow d))).tendsto' _ _ _).mono_left
    nhdsWithin_le_nhds
[GOAL]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ((fun x => x * ↑↑μ (interior s)) ∘ ENNReal.some ∘ fun a => a ^ d) 1 = ↑↑μ (interior s)
[PROOFSTEP]
simp


[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


[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.962
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : 0 < ∑ i in t, w i
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
⊢ f (centerMass t w p) ≤ centerMass t w (f ∘ p)
[PROOFSTEP]
have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} := fun i hi => ⟨hmem i hi, le_rfl⟩
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.962
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : 0 < ∑ i in t, w i
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
hmem' : ∀ (i : ι), i ∈ t → (p i, (f ∘ p) i) ∈ {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
⊢ f (centerMass t w p) ≤ centerMass t w (f ∘ p)
[PROOFSTEP]
convert (hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2
[GOAL]
case h.e'_3.h.e'_1
𝕜 : Type u_3
E : Type u_2
F : Type ?u.962
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : 0 < ∑ i in t, w i
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
hmem' : ∀ (i : ι), i ∈ t → (p i, (f ∘ p) i) ∈ {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
⊢ centerMass t w p = (centerMass t (fun i => w i) fun i => (p i, (f ∘ p) i)).fst
[PROOFSTEP]
simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]
[GOAL]
case h.e'_4
𝕜 : Type u_3
E : Type u_2
F : Type ?u.962
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : 0 < ∑ i in t, w i
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
hmem' : ∀ (i : ι), i ∈ t → (p i, (f ∘ p) i) ∈ {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
⊢ centerMass t w (f ∘ p) = (centerMass t (fun i => w i) fun i => (p i, (f ∘ p) i)).snd
[PROOFSTEP]
simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.21511
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : ∑ i in t, w i = 1
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
⊢ f (∑ i in t, w i • p i) ≤ ∑ i in t, w i • f (p i)
[PROOFSTEP]
simpa only [centerMass, h₁, inv_one, one_smul] using hf.map_centerMass_le h₀ (h₁.symm ▸ zero_lt_one) hmem
[GOAL]
𝕜 : Type u_3
E : Type u_1
F : Type ?u.35782
β : Type u_2
ι : Type ?u.35788
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f
hx : x ∈ ↑(convexHull 𝕜) ↑s
⊢ f x ≤ sup' s (_ : Finset.Nonempty s) f
[PROOFSTEP]
obtain ⟨w, hw₀, hw₁, rfl⟩ := mem_convexHull.1 hx
[GOAL]
case intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.35782
β : Type u_2
ι : Type ?u.35788
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜) ↑s
⊢ f (centerMass s w _root_.id) ≤ sup' s (_ : Finset.Nonempty s) f
[PROOFSTEP]
exact (hf.map_centerMass_le hw₀ (by positivity) <| subset_convexHull _ _).trans (centerMass_le_sup hw₀ <| by positivity)
[GOAL]
𝕜 : Type u_3
E : Type u_1
F : Type ?u.35782
β : Type u_2
ι : Type ?u.35788
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜) ↑s
⊢ 0 < ∑ i in s, w i
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_3
E : Type u_1
F : Type ?u.35782
β : Type u_2
ι : Type ?u.35788
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜) ↑s
⊢ 0 < ∑ i in s, w i
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
⊢ ∃ i, i ∈ t ∧ f (centerMass t w p) ≤ f (p i)
[PROOFSTEP]
set y := t.centerMass w p
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
⊢ ∃ i, i ∈ t ∧ f y ≤ f (p i)
[PROOFSTEP]
obtain ⟨i, hi, hfi⟩ : ∃ i ∈ t.filter fun i => w i ≠ 0, w i • f y ≤ w i • (f ∘ p) i
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
⊢ ∃ i, i ∈ filter (fun i => w i ≠ 0) t ∧ w i • f y ≤ w i • (f ∘ p) i
case intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
i : ι
hi : i ∈ filter (fun i => w i ≠ 0) t
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i, i ∈ t ∧ f y ≤ f (p i)
[PROOFSTEP]
rotate_left
[GOAL]
case intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
i : ι
hi : i ∈ filter (fun i => w i ≠ 0) t
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i, i ∈ t ∧ f y ≤ f (p i)
[PROOFSTEP]
rw [mem_filter] at hi
[GOAL]
case intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
i : ι
hi : i ∈ t ∧ w i ≠ 0
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i, i ∈ t ∧ f y ≤ f (p i)
[PROOFSTEP]
exact ⟨i, hi.1, (smul_le_smul_iff_of_pos <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
⊢ ∃ i, i ∈ filter (fun i => w i ≠ 0) t ∧ w i • f y ≤ w i • (f ∘ p) i
[PROOFSTEP]
have hw' : (0 : 𝕜) < ∑ i in filter (fun i => w i ≠ 0) t, w i := by rwa [sum_filter_ne_zero]
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
⊢ 0 < ∑ i in filter (fun i => w i ≠ 0) t, w i
[PROOFSTEP]
rwa [sum_filter_ne_zero]
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
hw' : 0 < ∑ i in filter (fun i => w i ≠ 0) t, w i
⊢ ∃ i, i ∈ filter (fun i => w i ≠ 0) t ∧ w i • f y ≤ w i • (f ∘ p) i
[PROOFSTEP]
refine' exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') _
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
hw' : 0 < ∑ i in filter (fun i => w i ≠ 0) t, w i
⊢ ∑ i in filter (fun i => w i ≠ 0) t, w i • f y ≤ ∑ i in filter (fun i => w i ≠ 0) t, w i • (f ∘ p) i
[PROOFSTEP]
rw [← sum_smul, ← smul_le_smul_iff_of_pos (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ← Finset.centerMass,
  Finset.centerMass_filter_ne_zero]
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
hw' : 0 < ∑ i in filter (fun i => w i ≠ 0) t, w i
⊢ f y ≤ centerMass t (fun i => w i) fun i => (f ∘ p) i
[PROOFSTEP]
exact h.map_centerMass_le hw₀ hw₁ hp
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.105120
β : Type u_1
ι : Type ?u.105126
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x✝ : E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ ∃ y, y ∈ s ∧ f x ≤ f y
[PROOFSTEP]
rw [_root_.convexHull_eq] at hx
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.105120
β : Type u_1
ι : Type ?u.105126
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x✝ : E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f
x : E
hx : x ∈ {x | ∃ ι t w z x_1 x_2 x_3, centerMass t w z = x}
⊢ ∃ y, y ∈ s ∧ f x ≤ f y
[PROOFSTEP]
obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.105120
β : Type u_1
ι : Type ?u.105126
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t✝ : Finset ι
w✝ : ι → 𝕜
p✝ : ι → E
x : E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ (i : α), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hp : ∀ (i : α), i ∈ t → p i ∈ s
⊢ ∃ y, y ∈ s ∧ f (centerMass t w p) ≤ f y
[PROOFSTEP]
rcases hf.exists_ge_of_centerMass hw₀ (hw₁.symm ▸ zero_lt_one) fun i hi => subset_convexHull 𝕜 s (hp i hi) with
  ⟨i, hit, Hi⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.105120
β : Type u_1
ι : Type ?u.105126
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t✝ : Finset ι
w✝ : ι → 𝕜
p✝ : ι → E
x : E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ (i : α), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hp : ∀ (i : α), i ∈ t → p i ∈ s
i : α
hit : i ∈ t
Hi : f (centerMass t (fun i => w i) fun i => p i) ≤ f (p i)
⊢ ∃ y, y ∈ s ∧ f (centerMass t w p) ≤ f y
[PROOFSTEP]
exact ⟨p i, hp i hit, Hi⟩


[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ intrinsicInterior 𝕜 ∅ = ∅
[PROOFSTEP]
simp [intrinsicInterior]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ intrinsicFrontier 𝕜 ∅ = ∅
[PROOFSTEP]
simp [intrinsicFrontier]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ intrinsicClosure 𝕜 ∅ = ∅
[PROOFSTEP]
simp [intrinsicClosure]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ Set.Nonempty (intrinsicClosure 𝕜 s) → Set.Nonempty s
[PROOFSTEP]
simp_rw [nonempty_iff_ne_empty]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ intrinsicClosure 𝕜 s ≠ ∅ → s ≠ ∅
[PROOFSTEP]
rintro h rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
t : Set P
x : P
h : intrinsicClosure 𝕜 ∅ ≠ ∅
⊢ False
[PROOFSTEP]
exact h intrinsicClosure_empty
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ x : P
⊢ intrinsicInterior 𝕜 {x} = {x}
[PROOFSTEP]
simpa only [intrinsicInterior, preimage_coe_affineSpan_singleton, interior_univ, image_univ, Subtype.range_coe] using
  coe_affineSpan_singleton _ _ _
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ x : P
⊢ intrinsicFrontier 𝕜 {x} = ∅
[PROOFSTEP]
rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ x : P
⊢ intrinsicClosure 𝕜 {x} = {x}
[PROOFSTEP]
simpa only [intrinsicClosure, preimage_coe_affineSpan_singleton, closure_univ, image_univ, Subtype.range_coe] using
  coe_affineSpan_singleton _ _ _
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
h : s ⊆ t
⊢ intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t
[PROOFSTEP]
refine' image_subset_iff.2 fun x hx => _
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ : P
h : s ⊆ t
x : { x // x ∈ affineSpan 𝕜 s }
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ x ∈ Subtype.val ⁻¹' intrinsicClosure 𝕜 t
[PROOFSTEP]
refine' ⟨Set.inclusion (affineSpan_mono _ h) x, _, rfl⟩
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ : P
h : s ⊆ t
x : { x // x ∈ affineSpan 𝕜 s }
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ inclusion (_ : affineSpan 𝕜 s ≤ affineSpan 𝕜 t) x ∈ closure (Subtype.val ⁻¹' t)
[PROOFSTEP]
refine' (continuous_inclusion (affineSpan_mono _ h)).closure_preimage_subset _ (closure_mono _ hx)
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ : P
h : s ⊆ t
x : { x // x ∈ affineSpan 𝕜 s }
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ Subtype.val ⁻¹' s ⊆ inclusion (_ : affineSpan 𝕜 s ≤ affineSpan 𝕜 t) ⁻¹' (Subtype.val ⁻¹' t)
[PROOFSTEP]
exact fun y hy => h hy
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ (fun a => ↑a) '' (closure (Subtype.val ⁻¹' s) \ frontier (Subtype.val ⁻¹' s)) = intrinsicInterior 𝕜 s
[PROOFSTEP]
rw [closure_diff_frontier, intrinsicInterior]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s
[PROOFSTEP]
simp [intrinsicClosure, intrinsicInterior, intrinsicFrontier, closure_eq_interior_union_frontier, image_union]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s
[PROOFSTEP]
rw [union_comm, intrinsicInterior_union_intrinsicFrontier]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
hs : IsClosed (Subtype.val ⁻¹' s)
⊢ intrinsicClosure 𝕜 s = s
[PROOFSTEP]
rw [intrinsicClosure, hs.closure_eq, image_preimage_eq_of_subset]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
hs : IsClosed (Subtype.val ⁻¹' s)
⊢ s ⊆ range Subtype.val
[PROOFSTEP]
exact (subset_affineSpan _ _).trans Subtype.range_coe.superset
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s
[PROOFSTEP]
refine' IsClosed.intrinsicClosure _
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
[PROOFSTEP]
set t := affineSpan 𝕜 (intrinsicClosure 𝕜 s) with ht
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t✝ : Set P
x : P
s : Set P
t : AffineSubspace 𝕜 P := affineSpan 𝕜 (intrinsicClosure 𝕜 s)
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
[PROOFSTEP]
clear_value t
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t✝ : Set P
x : P
s : Set P
t : AffineSubspace 𝕜 P
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
[PROOFSTEP]
obtain rfl := ht.trans (affineSpan_intrinsicClosure _)
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
[PROOFSTEP]
rw [intrinsicClosure, preimage_image_eq _ Subtype.coe_injective]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (closure (Subtype.val ⁻¹' s))
[PROOFSTEP]
exact isClosed_closure
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
⊢ intrinsicInterior 𝕜 (↑φ '' ∅) = ↑φ '' intrinsicInterior 𝕜 ∅
[PROOFSTEP]
simp only [intrinsicInterior_empty, image_empty]
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
haveI : Nonempty s := hs.to_subtype
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this✝ : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
this : ↑φ.toAffineMap ∘ Subtype.val ∘ ↑(Homeomorph.symm f) = Subtype.val
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
rw [intrinsicInterior, intrinsicInterior, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, ←
  Function.comp.assoc, image_comp, image_comp, f.symm.image_interior, f.image_symm, ← preimage_comp,
  Function.comp.assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp.right_id, preimage_comp,
  φ.injective.preimage_image]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
⊢ intrinsicFrontier 𝕜 (↑φ '' ∅) = ↑φ '' intrinsicFrontier 𝕜 ∅
[PROOFSTEP]
simp
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
haveI : Nonempty s := hs.to_subtype
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this✝ : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
this : ↑φ.toAffineMap ∘ Subtype.val ∘ ↑(Homeomorph.symm f) = Subtype.val
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
rw [intrinsicFrontier, intrinsicFrontier, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, ←
  Function.comp.assoc, image_comp, image_comp, f.symm.image_frontier, f.image_symm, ← preimage_comp,
  Function.comp.assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp.right_id, preimage_comp,
  φ.injective.preimage_image]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
⊢ intrinsicClosure 𝕜 (↑φ '' ∅) = ↑φ '' intrinsicClosure 𝕜 ∅
[PROOFSTEP]
simp
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
haveI : Nonempty s := hs.to_subtype
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this✝ : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
this : ↑φ.toAffineMap ∘ Subtype.val ∘ ↑(Homeomorph.symm f) = Subtype.val
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
rw [intrinsicClosure, intrinsicClosure, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, ← Function.comp.assoc,
  image_comp, image_comp, f.symm.image_closure, f.image_symm, ← preimage_comp, Function.comp.assoc, f.symm_comp_self,
  AffineIsometry.coe_toAffineMap, Function.comp.right_id, preimage_comp, φ.injective.preimage_image]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 s = closure s
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ x ∈ intrinsicClosure 𝕜 s ↔ x ∈ closure s
[PROOFSTEP]
simp only [mem_closure_iff, mem_intrinsicClosure]
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y, (∀ (o : Set { x // x ∈ affineSpan 𝕜 s }), IsOpen o → y ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)) ∧ ↑y = x) ↔
    ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
[PROOFSTEP]
refine' ⟨_, fun h => ⟨⟨x, _⟩, _, Subtype.coe_mk _ _⟩⟩
[GOAL]
case h.refine'_1
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y, (∀ (o : Set { x // x ∈ affineSpan 𝕜 s }), IsOpen o → y ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)) ∧ ↑y = x) →
    ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
[PROOFSTEP]
rintro ⟨x, h, rfl⟩ t ht hx
[GOAL]
case h.refine'_1.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : { x // x ∈ affineSpan 𝕜 s }
h : ∀ (o : Set { x // x ∈ affineSpan 𝕜 s }), IsOpen o → x ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)
t : Set P
ht : IsOpen t
hx : ↑x ∈ t
⊢ Set.Nonempty (t ∩ s)
[PROOFSTEP]
obtain ⟨z, hz₁, hz₂⟩ := h _ (continuous_induced_dom.isOpen_preimage t ht) hx
[GOAL]
case h.refine'_1.intro.intro.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : { x // x ∈ affineSpan 𝕜 s }
h : ∀ (o : Set { x // x ∈ affineSpan 𝕜 s }), IsOpen o → x ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)
t : Set P
ht : IsOpen t
hx : ↑x ∈ t
z : { x // x ∈ affineSpan 𝕜 s }
hz₁ : z ∈ Subtype.val ⁻¹' t
hz₂ : z ∈ Subtype.val ⁻¹' s
⊢ Set.Nonempty (t ∩ s)
[PROOFSTEP]
exact ⟨z, hz₁, hz₂⟩
[GOAL]
case h.refine'_2
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
⊢ ∀ (o : Set { x // x ∈ affineSpan 𝕜 s }),
    IsOpen o → { val := x, property := ?h.refine'_3 } ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)
[PROOFSTEP]
rintro _ ⟨t, ht, rfl⟩ hx
[GOAL]
case h.refine'_2.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
t : Set P
ht : IsOpen t
hx : { val := x, property := ?h.refine'_3 } ∈ Subtype.val ⁻¹' t
⊢ Set.Nonempty (Subtype.val ⁻¹' t ∩ Subtype.val ⁻¹' s)
[PROOFSTEP]
obtain ⟨y, hyt, hys⟩ := h _ ht hx
[GOAL]
case h.refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
t : Set P
ht : IsOpen t
hx : { val := x, property := ?h.refine'_3 } ∈ Subtype.val ⁻¹' t
y : P
hyt : y ∈ t
hys : y ∈ s
⊢ Set.Nonempty (Subtype.val ⁻¹' t ∩ Subtype.val ⁻¹' s)
[PROOFSTEP]
exact ⟨⟨_, subset_affineSpan 𝕜 s hys⟩, hyt, hys⟩
[GOAL]
case h.refine'_3
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
⊢ x ∈ ↑(affineSpan 𝕜 s)
[PROOFSTEP]
by_contra hc
[GOAL]
case h.refine'_3
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
hc : ¬x ∈ ↑(affineSpan 𝕜 s)
⊢ False
[PROOFSTEP]
obtain ⟨z, hz₁, hz₂⟩ := h _ (affineSpan 𝕜 s).closed_of_finiteDimensional.isOpen_compl hc
[GOAL]
case h.refine'_3.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
hc : ¬x ∈ ↑(affineSpan 𝕜 s)
z : P
hz₁ : z ∈ (↑(affineSpan 𝕜 s))ᶜ
hz₂ : z ∈ s
⊢ False
[PROOFSTEP]
exact hz₁ (subset_affineSpan 𝕜 s hz₂)
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ Set.Nonempty (interior s) ↔ Set.Nonempty (interior (↑φ ⁻¹' s))
[PROOFSTEP]
rw [← φ.image_symm, ← φ.symm.image_interior, nonempty_image_iff]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : Set.Nonempty s
⊢ Set.Nonempty (intrinsicInterior ℝ s)
[PROOFSTEP]
haveI := hsne.coe_sort
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : Set.Nonempty s
this : Nonempty ↑s
⊢ Set.Nonempty (intrinsicInterior ℝ s)
[PROOFSTEP]
obtain ⟨p, hp⟩ := hsne
[GOAL]
case intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
⊢ Set.Nonempty (intrinsicInterior ℝ s)
[PROOFSTEP]
let p' : _root_.affineSpan ℝ s := ⟨p, subset_affineSpan _ _ hp⟩
[GOAL]
case intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : { x // x ∈ _root_.affineSpan ℝ s } := { val := p, property := (_ : p ∈ ↑(_root_.affineSpan ℝ s)) }
⊢ Set.Nonempty (intrinsicInterior ℝ s)
[PROOFSTEP]
rw [intrinsicInterior, nonempty_image_iff, aux (AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph,
  Convex.interior_nonempty_iff_affineSpan_eq_top, AffineIsometryEquiv.coe_toHomeomorph, ←
  AffineIsometryEquiv.coe_toAffineEquiv, ← comap_span, affineSpan_coe_preimage_eq_top, comap_top]
[GOAL]
case intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : { x // x ∈ _root_.affineSpan ℝ s } := { val := p, property := (_ : p ∈ ↑(_root_.affineSpan ℝ s)) }
⊢ Convex ℝ
    (↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.symm (AffineIsometryEquiv.constVSub ℝ p'))) ⁻¹'
      (Subtype.val ⁻¹' s))
[PROOFSTEP]
exact
  hscv.affine_preimage
    ((_root_.affineSpan ℝ s).subtype.comp (AffineIsometryEquiv.constVSub ℝ p').symm.toAffineEquiv.toAffineMap)
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ Set.Nonempty (intrinsicInterior ℝ s) → Set.Nonempty s
[PROOFSTEP]
simp_rw [nonempty_iff_ne_empty]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ intrinsicInterior ℝ s ≠ ∅ → s ≠ ∅
[PROOFSTEP]
rintro h rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hs : Convex ℝ ∅
h : intrinsicInterior ℝ ∅ ≠ ∅
⊢ False
[PROOFSTEP]
exact h intrinsicInterior_empty