𝕜 : Type u_2
𝕝 : Type ?u.6609
E : Type u_1
F : Type ?u.6615
β : Type ?u.6618
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x y : E
a b : 𝕜
S : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) S
hS : ∀ (s : Set E), s ∈ S → StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃ (i : ↑S), ↑i)
𝕜 : Type u_2
𝕝 : Type ?u.6609
E : Type u_1
F : Type ?u.6615
β : Type ?u.6618
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x y : E
a b : 𝕜
S : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) S
hS : ∀ (s : Set E), s ∈ S → StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃₀ S)
rw [sUnion_eq_iUnion]
no goals
𝕜 : Type u_2
𝕝 : Type ?u.6609
E : Type u_1
F : Type ?u.6615
β : Type ?u.6618
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x y : E
a b : 𝕜
S : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) S
hS : ∀ (s : Set E), s ∈ S → StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃ (i : ↑S), ↑i)
exact (directedOn_iff_directed.1 hdir).strictConvex_iUnion fun s => hS _ s.2