𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Iio r
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r : β
⊢ Convex 𝕜 (Iio r)
intro x hx y hy a b ha hb hab
case inl
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ Iio r

case inr
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Iio r
obtain rfl | ha' := ha.eq_or_lt
case inr
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r
case inr
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r
rw [mem_Iio] at hx hy
no goals
case inr
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r
calc
  a • x + b • y < a • r + b • r :=
    add_lt_add_of_lt_of_le (smul_lt_smul_of_pos hx ha') (smul_le_smul_of_nonneg hy.le hb)
  _ = r := Convex.combo_self hab _
case inl
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ Iio r
case inl
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ Iio r
rw [zero_add] at hab
no goals
case inl
𝕜 : Type u_1
E : Type ?u.86645
F : Type ?u.86648
β : Type u_2
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ Iio r
rwa [zero_smul, zero_add, hab, one_smul]