internlm/Lean-Github huggingface dataset:
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
⊢ S ⊆ ↑(pointDual x')
Tactic:
intro s hs
Proof state after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
s : E
hs : s ∈ S
⊢ s ∈ ↑(pointDual x')
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
s : E
hs : s ∈ S
⊢ s ∈ ↑(pointDual x')
Tactic:
cases' (em (s = 0)) with h h
Proof state after:
case h.a.inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : s = 0
⊢ s ∈ ↑(pointDual x')

case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ s ∈ ↑(pointDual x')
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ s ∈ ↑(pointDual x')
Tactic:
specialize hx (pointDual ⟨ s, h ⟩) (Set.mem_image_of_mem _ ?_)
Proof state after:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ { val := s, property := h } ∈ Subtype.val ⁻¹' (S \ {0})

case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ↑(pointDual { val := s, property := h }).f x ≤ (pointDual { val := s, property := h }).α
⊢ s ∈ ↑(pointDual x')
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ↑(pointDual { val := s, property := h }).f x ≤ (pointDual { val := s, property := h }).α
⊢ s ∈ ↑(pointDual x')
Tactic:
rw [← Halfspace_mem, mem_pointDual, Subtype.coe_mk] at hx
Proof state after:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ⟪s, x⟫_ℝ ≤ 1
⊢ s ∈ ↑(pointDual x')
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ⟪s, x⟫_ℝ ≤ 1
⊢ s ∈ ↑(pointDual x')
Tactic:
rw [mem_pointDual, Subtype.coe_mk, real_inner_comm]
Proof state after:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ⟪s, x⟫_ℝ ≤ 1
⊢ ⟪s, x⟫_ℝ ≤ 1
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ⟪s, x⟫_ℝ ≤ 1
⊢ ⟪s, x⟫_ℝ ≤ 1
Tactic:
exact hx
Proof state after:
no goals
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : x = 0
⊢ x ∈ polarDual (Vpolytope hS)
Tactic:
rw [h]
Proof state after:
case h.a.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : x = 0
⊢ 0 ∈ polarDual (Vpolytope hS)
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : x = 0
⊢ 0 ∈ polarDual (Vpolytope hS)
Tactic:
exact polarDual_origin (Vpolytope hS)
Proof state after:
no goals
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
h : S ⊆ ↑(pointDual x')
⊢ p ∈ ↑(pointDual x')
Tactic:
apply convexHull_min h <| Halfspace_convex (pointDual x')
Proof state after:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
h : S ⊆ ↑(pointDual x')
⊢ p ∈ (convexHull ℝ) S
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
h : S ⊆ ↑(pointDual x')
⊢ p ∈ (convexHull ℝ) S
Tactic:
exact hp
Proof state after:
no goals
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : s = 0
⊢ s ∈ ↑(pointDual x')
Tactic:
exact h ▸ pointDual_origin x'
Proof state after:
no goals
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ { val := s, property := h } ∈ Subtype.val ⁻¹' (S \ {0})
Tactic:
rw [Set.mem_preimage, Subtype.coe_mk, Set.mem_diff]
Proof state after:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ s ∈ S ∧ s ∉ {0}
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ s ∈ S ∧ s ∉ {0}
Tactic:
exact ⟨ hs, h ⟩
Proof state after:
no goals
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ polarDual (Vpolytope hS) ⊆ Hpolytope ⋯
Tactic:
apply Set.sInter_subset_sInter
Proof state after:
case h.a.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' (S \ {0}))) ⊆
    SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' Vpolytope hS))
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' (S \ {0}))) ⊆
    SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' Vpolytope hS))
Tactic:
apply Set.image_subset
Proof state after:
case h.a.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ pointDual '' (Subtype.val ⁻¹' (S \ {0})) ⊆ pointDual '' (Subtype.val ⁻¹' Vpolytope hS)
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ pointDual '' (Subtype.val ⁻¹' (S \ {0})) ⊆ pointDual '' (Subtype.val ⁻¹' Vpolytope hS)
Tactic:
apply Set.image_subset
Proof state after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Subtype.val ⁻¹' (S \ {0}) ⊆ Subtype.val ⁻¹' Vpolytope hS
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Subtype.val ⁻¹' (S \ {0}) ⊆ Subtype.val ⁻¹' Vpolytope hS
Tactic:
rw [Set.preimage_subset_preimage_iff]
Proof state after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Vpolytope hS

case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Set.range Subtype.val
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Vpolytope hS

case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Set.range Subtype.val
Tactic:
apply subset_trans (by simp)  <| subset_convexHull _ _
Proof state after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Set.range Subtype.val
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Set.range Subtype.val
Tactic:
rw [Subtype.range_coe_subtype]
Proof state after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ {x | x ≠ 0}
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ {x | x ≠ 0}
Tactic:
intro x hx
Proof state after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S \ {0}
⊢ x ∈ {x | x ≠ 0}
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S \ {0}
⊢ x ∈ {x | x ≠ 0}
Tactic:
rw [Set.mem_diff, Set.mem_singleton_iff] at hx
Proof state after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S ∧ ¬x = 0
⊢ x ∈ {x | x ≠ 0}
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S ∧ ¬x = 0
⊢ x ∈ {x | x ≠ 0}
Tactic:
rw [Set.mem_setOf]
Proof state after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S ∧ ¬x = 0
⊢ x ≠ 0
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S ∧ ¬x = 0
⊢ x ≠ 0
Tactic:
exact hx.2
Proof state after:
no goals
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ S
Tactic:
simp
Proof state after:
no goals
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ ∀ {H_ : Set (Halfspace E)} (hH_ : Set.Finite H_),
    IsCompact (Hpolytope hH_) → ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Tactic:
intro H_ hH_ hHcpt
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
⊢ ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
⊢ ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Tactic:
have : closure (convexHull ℝ ((Hpolytope hH_).extremePoints ℝ)) = Hpolytope hH_ :=
  closure_convexHull_extremePoints hHcpt (Convex_Hpolytope hH_)
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Tactic:
rw [← this, IsClosed.closure_eq]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ ∃ S, ∃ (hS : Set.Finite S), (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hS

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ IsClosed ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ ∃ S, ∃ (hS : Set.Finite S), (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hS

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ IsClosed ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)))
Tactic:
use (Hpolytope hH_).extremePoints ℝ
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ ∃ (hS : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))),
    (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hS

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ IsClosed ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ ∃ (hS : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))),
    (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hS

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ IsClosed ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)))
Tactic:
use hExHFinite
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hExHFinite

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ IsClosed ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)))