internlm/Lean-Github huggingface dataset:
Theorem: ExtremePointsofHpolytope
Proof state before:
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_
Tactic:
specialize hsub (left_mem_segment ℝ x1 x2)
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
⊢ x1 ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
⊢ x1 ∈ ↑Hi_
Tactic:
rcases (em (Hi_ ∈ Hpolytope.I H_ x)) with (hinI | hninI)
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inl
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_

case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inr
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inl
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_
Tactic:
apply hmemsegmemI x1 ?_ Hi_ hinI
Proof state after:
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ segment ℝ (2 • x - y) y
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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ segment ℝ (2 • x - y) y
Tactic:
apply openSegment_subset_segment
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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ openSegment ℝ (2 • x - y) y
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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ openSegment ℝ (2 • x - y) y
Tactic:
exact Set.mem_of_mem_inter_left hsub
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inr
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_
Tactic:
have : Hi_ ∈ H_ \ Hpolytope.I H_ x := by
  rw [Set.mem_diff]
  exact ⟨ hHi_, hninI ⟩
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inr
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
this : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inr
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
this : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_
Tactic:
exact hmemballmemIc x1 (Set.mem_of_mem_inter_right hsub) Hi_ this
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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ \ Hpolytope.I H_ x
Tactic:
rw [Set.mem_diff]
Proof state after:
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ ∧ Hi_ ∉ 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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ ∧ Hi_ ∉ Hpolytope.I H_ x
Tactic:
exact ⟨ hHi_, hninI ⟩
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
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_
Tactic:
specialize hsub (right_mem_segment ℝ x1 x2)
Proof state after:
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
⊢ x2 ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
⊢ x2 ∈ ↑Hi_
Tactic:
rcases (em (Hi_ ∈ Hpolytope.I H_ x)) with (hinI | hninI)
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inl
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_

case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inr
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inl
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_
Tactic:
apply hmemsegmemI x2 ?_ Hi_ hinI
Proof state after:
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ segment ℝ (2 • x - y) y
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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ segment ℝ (2 • x - y) y
Tactic:
apply openSegment_subset_segment
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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ openSegment ℝ (2 • x - y) y
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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ openSegment ℝ (2 • x - y) y
Tactic:
exact Set.mem_of_mem_inter_left hsub
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inr
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_
Tactic:
have : Hi_ ∈ H_ \ Hpolytope.I H_ x := by
  rw [Set.mem_diff]
  exact ⟨ hHi_, hninI ⟩
Proof state after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inr
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
this : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inr
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
this : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_
Tactic:
exact hmemballmemIc x2 (Set.mem_of_mem_inter_right hsub) Hi_ this
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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ \ Hpolytope.I H_ x
Tactic:
rw [Set.mem_diff]
Proof state after:
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ ∧ Hi_ ∉ 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 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ ∧ Hi_ ∉ Hpolytope.I H_ x
Tactic:
exact ⟨ hHi_, hninI ⟩
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr
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_
⊢ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x} → x ∈ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
intro hinterx
Proof state after:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
rw [mem_extremePoints]
Proof state after:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ x ∈ Hpolytope hH_ ∧ ∀ x₁ ∈ Hpolytope hH_, ∀ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ x ∈ Hpolytope hH_ ∧ ∀ x₁ ∈ Hpolytope hH_, ∀ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x
Tactic:
refine ⟨ hxH, λ x1 hx1 x2 hx2 hx => ?_ ⟩
Proof state after:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ x1 = x ∧ x2 = x
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ x1 = x ∧ x2 = x
Tactic:
have : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x := by
  rw [Set.Nonempty.subset_singleton_iff (Set.nonempty_of_mem (left_mem_segment ℝ x1 x2)),
    Set.eq_singleton_iff_unique_mem]
  exact fun hseg => ⟨ hseg.2 x1 (left_mem_segment ℝ x1 x2),
    hseg.2 x2 (right_mem_segment ℝ x1 x2) ⟩
Proof state after:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
this : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
⊢ x1 = x ∧ x2 = x
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
this : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
⊢ x1 = x ∧ x2 = x
Tactic:
apply this
Proof state after:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
this : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
⊢ segment ℝ x1 x2 ⊆ {x}
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
this : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
⊢ segment ℝ x1 x2 ⊆ {x}
Tactic:
clear this
Proof state after:
case mpr
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_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ segment ℝ x1 x2 ⊆ {x}