internlm/Lean-Github huggingface dataset:
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
⊢ x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Tactic:
rintro HiS ⟨ Hi_, hHi_, rfl ⟩
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 ∈ ⋂₀ (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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x ∈ (fun x => interior ↑x) 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 ∈ ⋂₀ (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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x ∈ (fun x => interior ↑x) Hi_
Tactic:
rw [Set.mem_diff, Hpolytope.I_mem, IsClosed.frontier_eq <| Halfspace_closed Hi_,
  Set.mem_diff] at 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 ∈ ⋂₀ (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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ ∧ ¬(Hi_ ∈ H_ ∧ x ∈ ↑Hi_ ∧ x ∉ interior ↑Hi_)
⊢ x ∈ (fun x => interior ↑x) 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 ∈ ⋂₀ (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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ ∧ ¬(Hi_ ∈ H_ ∧ x ∈ ↑Hi_ ∧ x ∉ interior ↑Hi_)
⊢ x ∈ (fun x => interior ↑x) Hi_
Tactic:
push_neg at 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 ∈ ⋂₀ (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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ ∧ (Hi_ ∈ H_ → x ∈ ↑Hi_ → x ∈ interior ↑Hi_)
⊢ x ∈ (fun x => interior ↑x) 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 ∈ ⋂₀ (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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ ∧ (Hi_ ∈ H_ → x ∈ ↑Hi_ → x ∈ interior ↑Hi_)
⊢ x ∈ (fun x => interior ↑x) Hi_
Tactic:
exact hHi_.2 hHi_.1 <| hxH Hi_ ⟨ Hi_, hHi_.1, 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 ∈ ⋂₀ (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))
⊢ IsOpen (⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x)))
Tactic:
apply Set.Finite.isOpen_sInter (Set.Finite.image _ (Set.Finite.diff hH_ _))
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))
⊢ ∀ t ∈ (fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x), IsOpen t
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))
⊢ ∀ t ∈ (fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x), IsOpen t
Tactic:
exact fun _ ⟨ Hi_, _, h ⟩ => h ▸ isOpen_interior
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
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
Tactic:
rintro v hv Hi_ hHi_
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 ∈ 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_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ v ∈ ↑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
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_
Tactic:
rw [Set.mem_sInter] at hy
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 ∈ Hpolytope hH_
y : E
hy : ∀ t ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, y ∈ t
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ v ∈ ↑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 : ∀ t ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, y ∈ t
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_
Tactic:
specialize hy (frontier <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ frontier ↑Hi_
⊢ v ∈ ↑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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ frontier ↑Hi_
⊢ v ∈ ↑Hi_
Tactic:
have hHi_2 := hHi_.2
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ frontier ↑Hi_
hHi_2 : x ∈ frontier ↑Hi_
⊢ v ∈ ↑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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ frontier ↑Hi_
hHi_2 : x ∈ frontier ↑Hi_
⊢ v ∈ ↑Hi_
Tactic:
rw [frontierHalfspace_Hyperplane] at hy hHi_2
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ ↑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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ ↑Hi_
Tactic:
apply IsClosed.frontier_subset <| Halfspace_closed Hi_
Proof state after:
case 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ frontier ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ frontier ↑Hi_
Tactic:
rw [frontierHalfspace_Hyperplane]
Proof state after:
case 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ {x | ↑Hi_.f x = Hi_.α}
Theorem: ExtremePointsofHpolytope
Proof state before:
case 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
apply Set.mem_of_mem_of_subset hv
Proof state after:
case 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ (2 • x - y) y ⊆ {x | ↑Hi_.f x = Hi_.α}
Theorem: ExtremePointsofHpolytope
Proof state before:
case 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ (2 • x - y) y ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
apply (convex_iff_segment_subset.mp <| Hyperplane_convex Hi_) _ hy
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
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
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
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
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
h2x_y : (Finset.affineCombination ℝ Finset.univ ![x, y]) ![2, -1] ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
h2x_y : (Finset.affineCombination ℝ Finset.univ ![x, y]) ![2, -1] ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
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
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
h2x_y : 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
h2x_y : 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
exact h2x_y
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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ Finset.sum Finset.univ ![2, -1] = 1
Tactic:
rw [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 + -1 = 1
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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 + -1 = 1
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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ Set.range ![x, y] ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [Matrix.range_cons, Matrix.range_cons, Matrix.range_empty, Set.union_empty]
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 ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ {x} ∪ {y} ⊆ {x | ↑Hi_.f x = 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
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ {x} ∪ {y} ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
exact Set.union_subset (Set.singleton_subset_iff.mpr hHi_2) (Set.singleton_subset_iff.mpr hy)
Proof state after:
no goals