𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.32542
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : F
hx : x ∈ ↑f '' s
y : F
hy : y ∈ ↑f '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑f '' s
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.32542
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
⊢ Convex 𝕜 (↑f '' s)
intro x hx y hy a b ha hb hab
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.32542
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
y : F
hy : y ∈ ↑f '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : E
hx' : x' ∈ s
hx : ↑f x' ∈ ↑f '' s
⊢ a • ↑f x' + b • y ∈ ↑f '' s
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.32542
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : F
hx : x ∈ ↑f '' s
y : F
hy : y ∈ ↑f '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑f '' s
obtain ⟨x', hx', rfl⟩ := mem_image_iff_bex.1 hx
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.32542
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : E
hx' : x' ∈ s
hx : ↑f x' ∈ ↑f '' s
y' : E
hy' : y' ∈ s
hy : ↑f y' ∈ ↑f '' s
⊢ a • ↑f x' + b • ↑f y' ∈ ↑f '' s
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.32542
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
y : F
hy : y ∈ ↑f '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : E
hx' : x' ∈ s
hx : ↑f x' ∈ ↑f '' s
⊢ a • ↑f x' + b • y ∈ ↑f '' s
obtain ⟨y', hy', rfl⟩ := mem_image_iff_bex.1 hy
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type ?u.32542
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : E
hx' : x' ∈ s
hx : ↑f x' ∈ ↑f '' s
y' : E
hy' : y' ∈ s
hy : ↑f y' ∈ ↑f '' s
⊢ a • ↑f x' + b • ↑f y' ∈ ↑f '' s
exact ⟨a • x' + b • y', hs hx' 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
β : Type ?u.32542
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : E
hx' : x' ∈ s
hx : ↑f x' ∈ ↑f '' s
y' : E
hy' : y' ∈ s
hy : ↑f y' ∈ ↑f '' s
⊢ ↑f (a • x' + b • y') = a • ↑f x' + b • ↑f y'
rw [f.map_add, f.map_smul, f.map_smul]