𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
⊢ (⨅ (i : ι), innerDualCone (f i)) ≤ innerDualCone (⋃ (i : ι), f i)
𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
⊢ innerDualCone (⋃ (i : ι), f i) = ⨅ (i : ι), innerDualCone (f i)
refine' le_antisymm (le_iInf fun i x hx y hy => hx _ <| mem_iUnion_of_mem _ hy) _
𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
x : H
hx : x ∈ ⨅ (i : ι), innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
⊢ 0 ≤ inner y x
𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
⊢ (⨅ (i : ι), innerDualCone (f i)) ≤ innerDualCone (⋃ (i : ι), f i)
intro x hx y hy
𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
⊢ 0 ≤ inner y x
𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
x : H
hx : x ∈ ⨅ (i : ι), innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
⊢ 0 ≤ inner y x
rw [ConvexCone.mem_iInf] at hx
case intro
𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
j : ι
hj : y ∈ f j
⊢ 0 ≤ inner y x
𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
⊢ 0 ≤ inner y x
obtain ⟨j, hj⟩ := mem_iUnion.mp hy
no goals
case intro
𝕜 : Type ?u.15183
E : Type ?u.15186
F : Type ?u.15189
G : Type ?u.15192
H : Type u_2
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_1
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
j : ι
hj : y ∈ f j
⊢ 0 ≤ inner y x
exact hx _ _ hj