Theorem: mem_polarDual (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ v ∈ polarDual X ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Tactic:
unfold polarDual
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ v ∈ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))) ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ v ∈ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))) ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Tactic:
rw [Set.mem_sInter]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t) ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t) ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Tactic:
constructor
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t) → ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1) → ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t) → ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Tactic:
intro h x hx
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
⊢ ⟪x, v⟫_ℝ ≤ 1

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
cases' (em (x = 0)) with hx0 hx0
State after:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : x = 0
⊢ ⟪x, v⟫_ℝ ≤ 1

case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ⟪x, v⟫_ℝ ≤ 1

State before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
specialize h (SetLike.coe <| pointDual ⟨ x, hx0 ⟩) ?_
State after:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ↑(pointDual { val := x, property := hx0 }) ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))

case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v x : E
hx : x ∈ X
hx0 : ¬x = 0
h : v ∈ ↑(pointDual { val := x, property := hx0 })
⊢ ⟪x, v⟫_ℝ ≤ 1

State before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v x : E
hx : x ∈ X
hx0 : ¬x = 0
h : v ∈ ↑(pointDual { val := x, property := hx0 })
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
rw [mem_pointDual] at h
State after:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v x : E
hx : x ∈ X
hx0 : ¬x = 0
h : ⟪↑{ val := x, property := hx0 }, v⟫_ℝ ≤ 1
⊢ ⟪x, v⟫_ℝ ≤ 1

State before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v x : E
hx : x ∈ X
hx0 : ¬x = 0
h : ⟪↑{ val := x, property := hx0 }, v⟫_ℝ ≤ 1
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
exact h
State after:
no goals

State before:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : x = 0
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
rw [hx0, inner_zero_left]
State after:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : x = 0
⊢ 0 ≤ 1

State before:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : x = 0
⊢ 0 ≤ 1
Tactic:
exact zero_le_one
State after:
no goals

State before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ↑(pointDual { val := x, property := hx0 }) ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
Tactic:
apply Set.mem_image_of_mem
State after:
case mp.inr.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ pointDual { val := x, property := hx0 } ∈ pointDual '' (Subtype.val ⁻¹' X)

State before:
case mp.inr.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ pointDual { val := x, property := hx0 } ∈ pointDual '' (Subtype.val ⁻¹' X)
Tactic:
apply Set.mem_image_of_mem
State after:
case mp.inr.h.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ { val := x, property := hx0 } ∈ Subtype.val ⁻¹' X

State before:
case mp.inr.h.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ { val := x, property := hx0 } ∈ Subtype.val ⁻¹' X
Tactic:
rw [Set.mem_preimage]
State after:
case mp.inr.h.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ↑{ val := x, property := hx0 } ∈ X

State before:
case mp.inr.h.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ↑{ val := x, property := hx0 } ∈ X
Tactic:
exact hx
State after:
no goals

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1) → ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
Tactic:
intro h Hi_s hHi_s
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_s : Set E
hHi_s : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ v ∈ Hi_s

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_s : Set E
hHi_s : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ v ∈ Hi_s
Tactic:
rw [Set.mem_image] at hHi_s
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_s : Set E
hHi_s : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ v ∈ Hi_s

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_s : Set E
hHi_s : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ v ∈ Hi_s
Tactic:
rcases hHi_s with ⟨ Hi_, hHi_, rfl ⟩
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_ : Halfspace E
hHi_ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ v ∈ ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_ : Halfspace E
hHi_ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ v ∈ ↑Hi_
Tactic:
rw [Set.mem_image] at hHi_
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_ : Halfspace E
hHi_ : ∃ x ∈ Subtype.val ⁻¹' X, pointDual x = Hi_
⊢ v ∈ ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_ : Halfspace E
hHi_ : ∃ x ∈ Subtype.val ⁻¹' X, pointDual x = Hi_
⊢ v ∈ ↑Hi_
Tactic:
rcases hHi_ with ⟨ p, hp, rfl ⟩
State after:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
⊢ v ∈ ↑(pointDual p)

State before:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
⊢ v ∈ ↑(pointDual p)
Tactic:
specialize h p.1 hp
State after:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
h : ⟪↑p, v⟫_ℝ ≤ 1
⊢ v ∈ ↑(pointDual p)

State before:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
h : ⟪↑p, v⟫_ℝ ≤ 1
⊢ v ∈ ↑(pointDual p)
Tactic:
rw [mem_pointDual]
State after:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
h : ⟪↑p, v⟫_ℝ ≤ 1
⊢ ⟪↑p, v⟫_ℝ ≤ 1

State before:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
h : ⟪↑p, v⟫_ℝ ≤ 1
⊢ ⟪↑p, v⟫_ℝ ≤ 1
Tactic:
exact h
State after:
no goals