𝕜 : Type u_3
E : Type u_2
F : Type ?u.8423
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s✝ t : Set E
ι : Sort u_1
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : y ∈ ⋃ (i : ι), s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⋃ (i : ι), s i
𝕜 : Type u_3
E : Type u_2
F : Type ?u.8423
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s✝ t : Set E
ι : Sort u_1
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
⊢ StarConvex 𝕜 x (⋃ (i : ι), s i)
rintro y hy a b ha hb hab
𝕜 : Type u_3
E : Type u_2
F : Type ?u.8423
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s✝ t : Set E
ι : Sort u_1
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : ∃ i, y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ i, a • x + b • y ∈ s i
𝕜 : Type u_3
E : Type u_2
F : Type ?u.8423
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s✝ t : Set E
ι : Sort u_1
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : y ∈ ⋃ (i : ι), s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⋃ (i : ι), s i
rw [mem_iUnion] at hy⊢
case intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.8423
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s✝ t : Set E
ι : Sort u_1
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hy : y ∈ s i
⊢ ∃ i, a • x + b • y ∈ s i
𝕜 : Type u_3
E : Type u_2
F : Type ?u.8423
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s✝ t : Set E
ι : Sort u_1
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : ∃ i, y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ i, a • x + b • y ∈ s i
obtain ⟨i, hy⟩ := hy
no goals
case intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.8423
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s✝ t : Set E
ι : Sort u_1
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hy : y ∈ s i
⊢ ∃ i, a • x + b • y ∈ s i
exact ⟨i, hs i hy ha hb hab⟩