case h
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ innerDualCone ↑(innerDualCone ↑K) ↔ x ∈ K
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
⊢ innerDualCone ↑(innerDualCone ↑K) = K
ext x
case h.mp
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ innerDualCone ↑(innerDualCone ↑K) → x ∈ K

case h.mpr
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ K → x ∈ innerDualCone ↑(innerDualCone ↑K)
case h
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ innerDualCone ↑(innerDualCone ↑K) ↔ x ∈ K
constructor
case h.mp
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ (∀ (x_1 : H), x_1 ∈ ↑(innerDualCone ↑K) → 0 ≤ inner x_1 x) → x ∈ ↑K
case h.mp
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ innerDualCone ↑(innerDualCone ↑K) → x ∈ K
rw [mem_innerDualCone, ← SetLike.mem_coe]
case h.mp
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ ¬x ∈ ↑K → ∃ x_1, x_1 ∈ ↑(innerDualCone ↑K) ∧ inner x_1 x < 0
case h.mp
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ (∀ (x_1 : H), x_1 ∈ ↑(innerDualCone ↑K) → 0 ≤ inner x_1 x) → x ∈ ↑K
contrapose!
no goals
case h.mp
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ ¬x ∈ ↑K → ∃ x_1, x_1 ∈ ↑(innerDualCone ↑K) ∧ inner x_1 x < 0
exact K.hyperplane_separation_of_nonempty_of_isClosed_of_nmem ne hc
case h.mpr
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : y ∈ ↑(innerDualCone ↑K)
⊢ 0 ≤ inner y x
case h.mpr
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ K → x ∈ innerDualCone ↑(innerDualCone ↑K)
rintro hxK y h
case h.mpr
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : 0 ≤ inner x y
⊢ 0 ≤ inner y x
case h.mpr
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : y ∈ ↑(innerDualCone ↑K)
⊢ 0 ≤ inner y x
specialize h x hxK
no goals
case h.mpr
𝕜 : Type ?u.119420
E : Type ?u.119423
F : Type ?u.119426
G : Type ?u.119429
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : 0 ≤ inner x y
⊢ 0 ≤ inner y x
rwa [real_inner_comm]