𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ IsClosed (⋂ (i : ↑s), ↑(innerDualCone {↑i}))
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ IsClosed ↑(innerDualCone s)
rw [innerDualCone_eq_iInter_innerDualCone_singleton]
case h
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ∀ (i : ↑s), IsClosed ↑(innerDualCone {↑i})
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ IsClosed (⋂ (i : ↑s), ↑(innerDualCone {↑i}))
apply isClosed_iInter
case h
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
⊢ IsClosed ↑(innerDualCone {↑x})
case h
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ∀ (i : ↑s), IsClosed ↑(innerDualCone {↑i})
intro x
case h
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
h : ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
⊢ IsClosed ↑(innerDualCone {↑x})
case h
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
⊢ IsClosed ↑(innerDualCone {↑x})
have h : ({↑x} : Set H).innerDualCone = (inner x : H → ℝ) ⁻¹' Set.Ici 0 := by
  rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]
case h
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
h : ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
⊢ IsClosed (inner ↑x ⁻¹' Ici 0)
case h
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
h : ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
⊢ IsClosed ↑(innerDualCone {↑x})
rw [h]
no goals
case h
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
h : ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
⊢ IsClosed (inner ↑x ⁻¹' Ici 0)
exact isClosed_Ici.preimage (continuous_const.inner continuous_id')
no goals
𝕜 : Type ?u.21666
E : Type ?u.21669
F : Type ?u.21672
G : Type ?u.21675
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
⊢ ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]