Theorem: polarDual_comm_half (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
⊢ X ⊆ polarDual Y → Y ⊆ polarDual X
Tactic:
rw [Set.subset_def, Set.subset_def]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
⊢ (∀ x ∈ X, x ∈ polarDual Y) → ∀ x ∈ Y, x ∈ polarDual X

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
⊢ (∀ x ∈ X, x ∈ polarDual Y) → ∀ x ∈ Y, x ∈ polarDual X
Tactic:
intro h y hy
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
⊢ y ∈ polarDual X

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
⊢ y ∈ polarDual X
Tactic:
rw [mem_polarDual]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
⊢ ∀ x ∈ X, ⟪x, y⟫_ℝ ≤ 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
⊢ ∀ x ∈ X, ⟪x, y⟫_ℝ ≤ 1
Tactic:
intro x hx
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⟪x, y⟫_ℝ ≤ 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⟪x, y⟫_ℝ ≤ 1
Tactic:
rw [real_inner_comm]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⟪y, x⟫_ℝ ≤ 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⟪y, x⟫_ℝ ≤ 1
Tactic:
specialize h x hx
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : x ∈ polarDual Y
⊢ ⟪y, x⟫_ℝ ≤ 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : x ∈ polarDual Y
⊢ ⟪y, x⟫_ℝ ≤ 1
Tactic:
rw [mem_polarDual] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : ∀ x_1 ∈ Y, ⟪x_1, x⟫_ℝ ≤ 1
⊢ ⟪y, x⟫_ℝ ≤ 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : ∀ x_1 ∈ Y, ⟪x_1, x⟫_ℝ ≤ 1
⊢ ⟪y, x⟫_ℝ ≤ 1
Tactic:
specialize h y hy
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : ⟪y, x⟫_ℝ ≤ 1
⊢ ⟪y, x⟫_ℝ ≤ 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : ⟪y, x⟫_ℝ ≤ 1
⊢ ⟪y, x⟫_ℝ ≤ 1
Tactic:
exact h
State after:
no goals