𝕜 : Type u_2
E : Type u_1
F : Type ?u.8711
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s t : Set E
S : Set (Set E)
hS : ∀ (s : Set E), s ∈ S → StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃ (i : ↑S), ↑i)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8711
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s t : Set E
S : Set (Set E)
hS : ∀ (s : Set E), s ∈ S → StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃₀ S)
rw [sUnion_eq_iUnion]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8711
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
x : E
s t : Set E
S : Set (Set E)
hS : ∀ (s : Set E), s ∈ S → StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃ (i : ↑S), ↑i)
exact starConvex_iUnion fun s => hS _ s.2