Theorem: polarDual_convex (src/Polar.lean)

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

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ ∀ s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), Convex ℝ s
Tactic:
intro Hi_s h
State after:
case h
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))
⊢ Convex ℝ Hi_s

State before:
case h
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))
⊢ Convex ℝ Hi_s
Tactic:
rw [Set.mem_image] at h
State after:
case h
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
⊢ Convex ℝ Hi_s

State before:
case h
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
⊢ Convex ℝ Hi_s
Tactic:
rcases h with ⟨ Hi_, _, rfl ⟩
State after:
case h.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)
⊢ Convex ℝ ↑Hi_

State before:
case h.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)
⊢ Convex ℝ ↑Hi_
Tactic:
exact Halfspace_convex _
State after:
no goals