case mk.intro.mk.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.86134
α : Type ?u.86137
β : Type u_3
ι : Type ?u.86143
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : OrderedAddCommMonoid α
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).fst ∈ s
hr : f (x, r).fst ≤ (x, r).snd
y : E
t : β
hy : (y, t).fst ∈ s
ht : f (y, t).fst ≤ (y, t).snd
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x, r) + b • (y, t) ∈ {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
𝕜 : Type u_1
E : Type u_2
F : Type ?u.86134
α : Type ?u.86137
β : Type u_3
ι : Type ?u.86143
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : OrderedAddCommMonoid α
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
⊢ Convex 𝕜 {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
rintro ⟨x, r⟩ ⟨hx, hr⟩ ⟨y, t⟩ ⟨hy, ht⟩ a b ha hb hab
case mk.intro.mk.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.86134
α : Type ?u.86137
β : Type u_3
ι : Type ?u.86143
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : OrderedAddCommMonoid α
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).fst ∈ s
hr : f (x, r).fst ≤ (x, r).snd
y : E
t : β
hy : (y, t).fst ∈ s
ht : f (y, t).fst ≤ (y, t).snd
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • (x, r) + b • (y, t)).fst ≤ (a • (x, r) + b • (y, t)).snd
case mk.intro.mk.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.86134
α : Type ?u.86137
β : Type u_3
ι : Type ?u.86143
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : OrderedAddCommMonoid α
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).fst ∈ s
hr : f (x, r).fst ≤ (x, r).snd
y : E
t : β
hy : (y, t).fst ∈ s
ht : f (y, t).fst ≤ (y, t).snd
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x, r) + b • (y, t) ∈ {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
refine' ⟨hf.1 hx hy ha hb hab, _⟩
no goals
case mk.intro.mk.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.86134
α : Type ?u.86137
β : Type u_3
ι : Type ?u.86143
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : OrderedAddCommMonoid α
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).fst ∈ s
hr : f (x, r).fst ≤ (x, r).snd
y : E
t : β
hy : (y, t).fst ∈ s
ht : f (y, t).fst ≤ (y, t).snd
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • (x, r) + b • (y, t)).fst ≤ (a • (x, r) + b • (y, t)).snd
calc
  f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
  _ ≤ a • r + b • t := by gcongr
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.86134
α : Type ?u.86137
β : Type u_3
ι : Type ?u.86143
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : OrderedAddCommMonoid α
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).fst ∈ s
hr : f (x, r).fst ≤ (x, r).snd
y : E
t : β
hy : (y, t).fst ∈ s
ht : f (y, t).fst ≤ (y, t).snd
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • r + b • t
gcongr