𝕜 : 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
x y✝ z : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : F
hy : y ∈ ↑f '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • ↑f x + b • y ∈ ↑f '' s
𝕜 : 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
x y z : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
⊢ StarConvex 𝕜 (↑f x) (↑f '' s)
intro y hy a b ha hb hab
case intro.intro
𝕜 : 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
x y z : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • ↑f x + b • ↑f y' ∈ ↑f '' s
𝕜 : 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
x y✝ z : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : F
hy : y ∈ ↑f '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • ↑f x + b • y ∈ ↑f '' s
obtain ⟨y', hy', rfl⟩ := hy
no goals
case intro.intro
𝕜 : 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
x y z : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • ↑f x + b • ↑f y' ∈ ↑f '' s
exact ⟨a • x + b • y', hs hy' ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩
no goals
𝕜 : 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
x y z : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ ↑f (a • x + b • y') = a • ↑f x + b • ↑f y'
rw [f.map_add, f.map_smul, f.map_smul]