ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ fun ⦃a b⦄ => Set.Nonempty ([a-[𝕜]b] \ frontier s) → ∃ c, ↑(lineMap a b) c ∈ interior s
ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
⊢ StrictConvex 𝕜 s
refine' hs.strictConvex' <| h.imp_on fun x hx y hy _ => _
ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ Set.Nonempty ((fun a => ↑(lineMap x y) a) '' Icc 0 1 \ frontier s) → ∃ c, ↑(lineMap x y) c ∈ s \ frontier s
ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ fun ⦃a b⦄ => Set.Nonempty ([a-[𝕜]b] \ frontier s) → ∃ c, ↑(lineMap a b) c ∈ interior s
simp only [segment_eq_image_lineMap, ← self_diff_frontier]
case intro.intro.intro.intro
ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : ¬(fun a => ↑(lineMap x y) a) c ∈ frontier s
⊢ ∃ c, ↑(lineMap x y) c ∈ s \ frontier s
ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ Set.Nonempty ((fun a => ↑(lineMap x y) a) '' Icc 0 1 \ frontier s) → ∃ c, ↑(lineMap x y) c ∈ s \ frontier s
rintro ⟨_, ⟨⟨c, hc, rfl⟩, hcs⟩⟩
case intro.intro.intro.intro
ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : ¬(fun a => ↑(lineMap x y) a) c ∈ frontier s
⊢ ↑(lineMap x y) c ∈ [x-[𝕜]y]
case intro.intro.intro.intro
ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : ¬(fun a => ↑(lineMap x y) a) c ∈ frontier s
⊢ ∃ c, ↑(lineMap x y) c ∈ s \ frontier s
refine' ⟨c, hs.segment_subset hx.1 hy.1 _, hcs⟩
no goals
case intro.intro.intro.intro
ι : Type ?u.151565
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : ¬(fun a => ↑(lineMap x y) a) c ∈ frontier s
⊢ ↑(lineMap x y) c ∈ [x-[𝕜]y]
exact (segment_eq_image_lineMap 𝕜 x y).symm ▸ mem_image_of_mem _ hc