ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
⊢ ∀ (x : E), x ∈ s → ∀ (y : E), y ∈ s → JoinedIn s x y
ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
⊢ IsPathConnected s
refine' isPathConnected_iff.mpr ⟨hne, _⟩
ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ JoinedIn s x y
ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
⊢ ∀ (x : E), x ∈ s → ∀ (y : E), y ∈ s → JoinedIn s x y
intro x x_in y y_in
ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
H : [x-[ℝ]y] ⊆ s
⊢ JoinedIn s x y
ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ JoinedIn s x y
have H := hconv.segment_subset x_in y_in
ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
H : ↑(lineMap x y) '' Icc 0 1 ⊆ s
⊢ JoinedIn s x y
ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
H : [x-[ℝ]y] ⊆ s
⊢ JoinedIn s x y
rw [segment_eq_image_lineMap] at H
no goals
ι : Type ?u.191359
𝕜 : Type ?u.191362
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
H : ↑(lineMap x y) '' Icc 0 1 ⊆ s
⊢ JoinedIn s x y
exact
  JoinedIn.ofLine AffineMap.lineMap_continuous.continuousOn (lineMap_apply_zero _ _)
    (lineMap_apply_one _ _) H