case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.240342
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ StarConvex 𝕜 (↑f x) (↑f '' s)
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.240342
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
⊢ Convex 𝕜 (↑f '' s)
rintro _ ⟨x, hx, rfl⟩
no goals
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.240342
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ StarConvex 𝕜 (↑f x) (↑f '' s)
exact (hs hx).affine_image _