internlm/Lean-Github huggingface dataset:
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ Hi_.α ≤ Hi_.α
Tactic:
linarith
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ 0 < 1 - t
Tactic:
linarith [ht.2]
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
⊢ False
Tactic:
rw [openSegment_symm, openSegment_eq_image', Set.mem_image] at hx
Proof state after:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : ∃ x_1 ∈ Set.Ioo 0 1, x2 + x_1 • (x1 - x2) = x
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
⊢ False
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : ∃ x_1 ∈ Set.Ioo 0 1, x2 + x_1 • (x1 - x2) = x
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
⊢ False
Tactic:
rcases hx with ⟨ t, ht, rfl ⟩
Proof state after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f (x2 + t • (x1 - x2)) = Hi_.α
⊢ False
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f (x2 + t • (x1 - x2)) = Hi_.α
⊢ False
Tactic:
rw [Hi_.f.1.map_add, Hi_.f.1.map_smul] at hfxα
Proof state after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ False
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ False
Tactic:
have : Hi_.f.1 x2 + t • Hi_.f.1 (x1 - x2) + (1-t) • Hi_.f.1 (x1 - x2) > Hi_.α := by
  rw [hfxα, gt_iff_lt]
  exact lt_add_of_le_of_pos (by linarith) <|
    (smul_pos_iff_of_pos_left (by linarith [ht.2])).mpr <|
    (smul_pos_iff_of_pos_left ht.1).mp <| pos_of_lt_add_right <| hfxα.symm ▸ hlt
Proof state after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
this : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) + (1 - t) • ↑Hi_.f (x1 - x2) > Hi_.α
⊢ False
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
this : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) + (1 - t) • ↑Hi_.f (x1 - x2) > Hi_.α
⊢ False
Tactic:
rw [add_assoc, ← add_smul, add_sub, add_comm t 1, add_sub_cancel, one_smul,
  ← Hi_.f.1.map_add, add_comm, sub_add_cancel] at this
Proof state after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
this : ↑Hi_.f x1 > Hi_.α
⊢ False
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
this : ↑Hi_.f x1 > Hi_.α
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) + (1 - t) • ↑Hi_.f (x1 - x2) > Hi_.α
Tactic:
rw [hfxα, gt_iff_lt]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ Hi_.α < Hi_.α + (1 - t) • ↑Hi_.f (x1 - x2)
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ Hi_.α < Hi_.α + (1 - t) • ↑Hi_.f (x1 - x2)
Tactic:
exact lt_add_of_le_of_pos (by linarith) <|
  (smul_pos_iff_of_pos_left (by linarith [ht.2])).mpr <|
  (smul_pos_iff_of_pos_left ht.1).mp <| pos_of_lt_add_right <| hfxα.symm ▸ hlt
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ Hi_.α ≤ Hi_.α
Tactic:
linarith
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ 0 < 1 - t
Tactic:
linarith [ht.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)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)
Tactic:
suffices hHeqVdual : ∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite),
  Hpolytope hH_ = polarDual (Vpolytope hS) from by
  rcases hHeqVdual with ⟨H_, hH_, hHeqVdual⟩
  refine ⟨ H_, hH_, hHeqVdual, ?_ ⟩
  exact hHeqVdual ▸ (polarDual_compact_if (Closed_Vpolytope hS) (Convex_Vpolytope hS) hS0)
Proof state after:
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)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS)
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)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS)
Tactic:
use pointDual '' (Subtype.val ⁻¹' (S \ {0}))
Proof state after:
case 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)
⊢ ∃ (hH_ : Set.Finite (pointDual '' (Subtype.val ⁻¹' (S \ {0})))), Hpolytope hH_ = polarDual (Vpolytope hS)
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case 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)
⊢ ∃ (hH_ : Set.Finite (pointDual '' (Subtype.val ⁻¹' (S \ {0})))), Hpolytope hH_ = polarDual (Vpolytope hS)
Tactic:
use (by
  apply Set.Finite.image
  apply Set.Finite.preimage _ _
  apply Set.injOn_of_injective
  exact Subtype.val_injective
  exact Set.Finite.diff hS {0}
  done)
Proof state after:
case 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)
⊢ Hpolytope ⋯ = polarDual (Vpolytope hS)
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case 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)
⊢ Hpolytope ⋯ = polarDual (Vpolytope hS)
Tactic:
apply subset_antisymm
Proof state after:
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)
⊢ Hpolytope ⋯ ⊆ polarDual (Vpolytope hS)

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 ⋯
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)
hHeqVdual : ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)
Tactic:
rcases hHeqVdual with ⟨H_, hH_, hHeqVdual⟩
Proof state after:
case intro.intro
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)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHeqVdual : Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case intro.intro
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)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHeqVdual : Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)
Tactic:
refine ⟨ H_, hH_, hHeqVdual, ?_ ⟩
Proof state after:
case intro.intro
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)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHeqVdual : Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ IsCompact (Hpolytope hH_)
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case intro.intro
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)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHeqVdual : Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ IsCompact (Hpolytope hH_)
Tactic:
exact hHeqVdual ▸ (polarDual_compact_if (Closed_Vpolytope hS) (Convex_Vpolytope hS) hS0)
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)
⊢ Set.Finite (pointDual '' (Subtype.val ⁻¹' (S \ {0})))
Tactic:
apply Set.Finite.image
Proof state after:
case hs
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)
⊢ Set.Finite (Subtype.val ⁻¹' (S \ {0}))
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case hs
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)
⊢ Set.Finite (Subtype.val ⁻¹' (S \ {0}))
Tactic:
apply Set.Finite.preimage _ _
Proof state after:
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)
⊢ Set.InjOn Subtype.val (Subtype.val ⁻¹' (S \ {0}))

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)
⊢ Set.Finite (S \ {0})
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)
⊢ Set.InjOn Subtype.val (Subtype.val ⁻¹' (S \ {0}))

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)
⊢ Set.Finite (S \ {0})
Tactic:
apply Set.injOn_of_injective
Proof state after:
case 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)
⊢ Function.Injective Subtype.val

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)
⊢ Set.Finite (S \ {0})
Theorem: DualOfVpolytope_compactHpolytope
Proof state before:
case 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)
⊢ Function.Injective Subtype.val

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)
⊢ Set.Finite (S \ {0})
Tactic:
exact Subtype.val_injective
Proof state after:
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)
⊢ Set.Finite (S \ {0})
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)
⊢ Set.Finite (S \ {0})
Tactic:
exact Set.Finite.diff hS {0}
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)
⊢ Hpolytope ⋯ ⊆ polarDual (Vpolytope hS)
Tactic:
intro x hx
Proof state after:
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)
x : E
hx : x ∈ Hpolytope ⋯
⊢ x ∈ polarDual (Vpolytope hS)
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)
x : E
hx : x ∈ Hpolytope ⋯
⊢ x ∈ polarDual (Vpolytope hS)
Tactic:
cases' (em (x = 0)) with h 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
⊢ x ∈ polarDual (Vpolytope hS)

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 : x ∈ Hpolytope ⋯
h : ¬x = 0
⊢ x ∈ polarDual (Vpolytope hS)
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 : x ∈ Hpolytope ⋯
h : ¬x = 0
⊢ x ∈ polarDual (Vpolytope hS)
Tactic:
rw [mem_Hpolytope] at hx
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
⊢ x ∈ polarDual (Vpolytope hS)
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
⊢ x ∈ polarDual (Vpolytope hS)
Tactic:
rw [mem_polarDual]
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
⊢ ∀ x_1 ∈ Vpolytope hS, ⟪x_1, x⟫_ℝ ≤ 1
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
⊢ ∀ x_1 ∈ Vpolytope hS, ⟪x_1, x⟫_ℝ ≤ 1
Tactic:
intro p hp
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
⊢ ⟪p, x⟫_ℝ ≤ 1
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
⊢ ⟪p, x⟫_ℝ ≤ 1
Tactic:
let x' := (⟨ x, h ⟩ : { p : E // p ≠ 0 })
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 }
⊢ ⟪p, x⟫_ℝ ≤ 1
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 }
⊢ ⟪p, x⟫_ℝ ≤ 1
Tactic:
have hx' : ↑x' = x := rfl
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
⊢ ⟪p, x⟫_ℝ ≤ 1
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
⊢ ⟪p, x⟫_ℝ ≤ 1
Tactic:
rw [← hx', real_inner_comm, ←mem_pointDual]
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
⊢ p ∈ ↑(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
⊢ p ∈ ↑(pointDual x')
Tactic:
suffices h : S ⊆ SetLike.coe (pointDual x') from by
  apply convexHull_min h <| Halfspace_convex (pointDual x')
  exact hp
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 ⊆ ↑(pointDual x')