internlm/Lean-Github huggingface dataset:
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
have hmemsegmemI : ∀ v, v ∈ segment ℝ ((2:ℝ) • x - y) y →
  ∀ Hi_, Hi_ ∈ Hpolytope.I H_ x → v ∈ SetLike.coe Hi_ := by
  rintro v hv Hi_ hHi_
  rw [Set.mem_sInter] at hy
  specialize hy (frontier <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
  have hHi_2 := hHi_.2
  rw [frontierHalfspace_Hyperplane] at hy hHi_2
  apply IsClosed.frontier_subset <| Halfspace_closed Hi_
  rw [frontierHalfspace_Hyperplane]
  apply Set.mem_of_mem_of_subset hv
  apply (convex_iff_segment_subset.mp <| Hyperplane_convex Hi_) _ hy
  have h21 : Finset.sum Finset.univ ![(2:ℝ), -1] = 1 := by
    rw [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
    linarith
    done
  have h2x_y := Hyperplane_affineClosed Hi_ ![x, y] (by
    rw [Matrix.range_cons, Matrix.range_cons, Matrix.range_empty, Set.union_empty];
    exact Set.union_subset (Set.singleton_subset_iff.mpr hHi_2) (Set.singleton_subset_iff.mpr hy))
    ![2, -1] h21
  rw [Finset.affineCombination_eq_linear_combination _ _ _ h21, Fin.sum_univ_two, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.head_cons, neg_one_smul, ← sub_eq_add_neg] at h2x_y
  exact h2x_y
Proof state after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
rw [mem_extremePoints]
Proof state after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ¬(x ∈ Hpolytope hH_ ∧ ∀ x₁ ∈ Hpolytope hH_, ∀ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ¬(x ∈ Hpolytope hH_ ∧ ∀ x₁ ∈ Hpolytope hH_, ∀ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x)
Tactic:
push_neg
Proof state after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∈ Hpolytope hH_ → ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∈ Hpolytope hH_ → ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
rintro hxH'
Proof state after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
rcases hmemballmemIc with ⟨ ε, hε, hmemballmemIc ⟩
Proof state after:
case mp.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
rcases hxSegBallInterSeg ((2:ℝ) • x - y) y ε ⟨ hxyy, fun h => hyx h.2 ⟩ hε with
  ⟨ x1, x2, hmem, hsub, hne ⟩
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : ¬(x1 = x ∧ x2 = x)
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : ¬(x1 = x ∧ x2 = x)
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
push_neg at hne
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
clear hxH' hε hyx hy hxH hxyy
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
unfold Hpolytope
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ ⋂₀ (SetLike.coe '' H_), ∃ x₂ ∈ ⋂₀ (SetLike.coe '' H_), x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ ⋂₀ (SetLike.coe '' H_), ∃ x₂ ∈ ⋂₀ (SetLike.coe '' H_), x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
refine ⟨ x1, ?_, x2, ?_, ⟨ hmem, hne ⟩ ⟩ <;> clear hmem hne <;>
rw [Set.mem_sInter] <;>
intro Hi_s hHi_s <;>
rw [Set.mem_image] at hHi_s <;>
rcases hHi_s with ⟨ Hi_, hHi_, rfl ⟩
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x1 ∈ ↑Hi_

case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x2 ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
⊢ x ∈ openSegment ℝ (2 • x - y) y
Tactic:
clear hyx hy hxH hH_
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ x ∈ openSegment ℝ (2 • x - y) y
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ x ∈ openSegment ℝ (2 • x - y) y
Tactic:
rw [openSegment_eq_image, Set.mem_image]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ ∃ x_1 ∈ Set.Ioo 0 1, (1 - x_1) • (2 • x - y) + x_1 • y = x
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ ∃ x_1 ∈ Set.Ioo 0 1, (1 - x_1) • (2 • x - y) + x_1 • y = x
Tactic:
refine ⟨ 1/2, by norm_num, ?_ ⟩
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ (1 - 1 / 2) • (2 • x - y) + (1 / 2) • y = x
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ (1 - 1 / 2) • (2 • x - y) + (1 / 2) • y = x
Tactic:
rw [(by norm_num : (1:ℝ) - 1 / 2 = 1 / 2), smul_sub, sub_add_cancel, smul_smul,
  div_mul_cancel _ (by linarith), one_smul]
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ 1 / 2 ∈ Set.Ioo 0 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ 1 - 1 / 2 = 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ 2 ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hball : ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
Tactic:
rcases hball with ⟨ ε, hε, hball ⟩
Proof state after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
Tactic:
refine ⟨ ε, hε, fun v hv Hi_ hHi_ => ?_ ⟩
Proof state after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
v : E
hv : v ∈ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
v : E
hv : v ∈ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_
Tactic:
apply interior_subset
Proof state after:
case intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
v : E
hv : v ∈ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ v ∈ interior ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
v : E
hv : v ∈ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ v ∈ interior ↑Hi_
Tactic:
exact (Set.mem_sInter.mp <| hball hv) (interior <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Tactic:
unfold Hpolytope at hxH
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
hIcinteriorOpen : IsOpen (⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x)))
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Tactic:
rw [Metric.isOpen_iff] at hIcinteriorOpen
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
hIcinteriorOpen :
  ∀ x_1 ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x)),
    ∃ ε > 0, Metric.ball x_1 ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
hIcinteriorOpen :
  ∀ x_1 ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x)),
    ∃ ε > 0, Metric.ball x_1 ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Tactic:
exact hIcinteriorOpen x hxIcinterior
Proof state after:
no goals