Theorem: polarDual_closed (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ IsClosed (polarDual X)
Tactic:
apply isClosed_sInter
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), IsClosed t

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), IsClosed t
Tactic:
intro Hi_s h
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ IsClosed Hi_s

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ IsClosed Hi_s
Tactic:
rw [Set.mem_image] at h
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ IsClosed Hi_s

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ IsClosed Hi_s
Tactic:
rcases h with ⟨ Hi_, _, rfl ⟩
State after:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
left✝ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ IsClosed ↑Hi_

State before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
left✝ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ IsClosed ↑Hi_
Tactic:
exact Halfspace_closed _
State after:
no goals