Theorem: polarDual_compact_if (src/Polar.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
⊢ 0 ∈ interior X → IsCompact (polarDual X)
Tactic:
intro h
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
h : 0 ∈ interior X
⊢ IsCompact (polarDual X)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
h : 0 ∈ interior X
⊢ IsCompact (polarDual X)
Tactic:
rw [← doublePolarDual_self hXcl hXcv (interior_subset h), compact_polarDual_iff (polarDual_closed _)] at h
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
h : IsCompact (polarDual X)
⊢ IsCompact (polarDual X)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
h : IsCompact (polarDual X)
⊢ IsCompact (polarDual X)
Tactic:
exact h
State after:
no goals