𝕜 : Type u_2
E : Type u_1
F : Type ?u.8386
β : Type ?u.8389
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x : E
c : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃ (i : ↑c), ↑i)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8386
β : Type ?u.8389
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x : E
c : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃₀ c)
rw [sUnion_eq_iUnion]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8386
β : Type ?u.8389
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x : E
c : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃ (i : ↑c), ↑i)
exact (directedOn_iff_directed.1 hdir).convex_iUnion fun A => hc A.2