internlm/Lean-Github huggingface dataset:
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
⊢ segment ℝ x1 x2 ⊆ {x}
Tactic:
rw [← hinterx, Set.subset_sInter_iff]
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
⊢ ∀ t' ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, segment ℝ x1 x2 ⊆ t'
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
⊢ ∀ t' ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, segment ℝ x1 x2 ⊆ t'
Tactic:
rintro HiS ⟨ Hi_, hHi_, rfl ⟩
Proof state after:
case mpr.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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ segment ℝ x1 x2 ⊆ (fun x => frontier ↑x) Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ segment ℝ x1 x2 ⊆ (fun x => frontier ↑x) Hi_
Tactic:
simp only
Proof state after:
case mpr.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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
have hfxα : Hi_.f.1 x = Hi_.α := by
  have : x ∈ {x} := by
    exact Set.mem_singleton x
  rw [← hinterx, Set.mem_sInter] at this
  specialize this (frontier <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
  rw [frontierHalfspace_Hyperplane, Set.mem_setOf] at this
  exact this
Proof state after:
case mpr.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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
clear hinterx hxH
Proof state after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
rw [mem_Hpolytope] at hx1 hx2
Proof state after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 : E
hx1 : ∀ Hi ∈ H_, ↑Hi.f x1 ≤ Hi.α
x2 : E
hx2 : ∀ Hi ∈ H_, ↑Hi.f x2 ≤ Hi.α
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 : E
hx1 : ∀ Hi ∈ H_, ↑Hi.f x1 ≤ Hi.α
x2 : E
hx2 : ∀ Hi ∈ H_, ↑Hi.f x2 ≤ Hi.α
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
specialize hx1 Hi_ hHi_.1
Proof state after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 x2 : E
hx2 : ∀ Hi ∈ H_, ↑Hi.f x2 ≤ Hi.α
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 x2 : E
hx2 : ∀ Hi ∈ H_, ↑Hi.f x2 ≤ Hi.α
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
specialize hx2 Hi_ hHi_.1
Proof state after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
clear hHi_ hH_ H_
Proof state after:
case mpr.intro.intro
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_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro
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_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
rw [frontierHalfspace_Hyperplane]
Proof state after:
case mpr.intro.intro
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_.α
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro
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_.α
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
have := Hyperplane_convex Hi_
Proof state after:
case mpr.intro.intro
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_.α
this : Convex ℝ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro
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_.α
this : Convex ℝ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [convex_iff_segment_subset] at this
Proof state after:
case mpr.intro.intro
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_.α
this :
  ∀ ⦃x : E⦄, x ∈ {x | ↑Hi_.f x = Hi_.α} → ∀ ⦃y : E⦄, y ∈ {x | ↑Hi_.f x = Hi_.α} → segment ℝ x y ⊆ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Theorem: ExtremePointsofHpolytope
Proof state before:
case mpr.intro.intro
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_.α
this :
  ∀ ⦃x : E⦄, x ∈ {x | ↑Hi_.f x = Hi_.α} → ∀ ⦃y : E⦄, y ∈ {x | ↑Hi_.f x = Hi_.α} → segment ℝ x y ⊆ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
apply this <;>
clear this <;>
rw [Set.mem_setOf] <;>
by_contra h <;>
push_neg at h <;>
have hlt := lt_of_le_of_ne (by assumption) h <;>
clear h
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 ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
⊢ False

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
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_
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} → x1 = x ∧ x2 = x
Tactic:
rw [Set.Nonempty.subset_singleton_iff (Set.nonempty_of_mem (left_mem_segment ℝ x1 x2)),
  Set.eq_singleton_iff_unique_mem]
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_
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
⊢ (x ∈ segment ℝ x1 x2 ∧ ∀ x_1 ∈ segment ℝ x1 x2, x_1 = x) → x1 = x ∧ x2 = 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 ∈ 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
⊢ (x ∈ segment ℝ x1 x2 ∧ ∀ x_1 ∈ segment ℝ x1 x2, x_1 = x) → x1 = x ∧ x2 = x
Tactic:
exact fun hseg => ⟨ hseg.2 x1 (left_mem_segment ℝ x1 x2),
  hseg.2 x2 (right_mem_segment ℝ x1 x2) ⟩
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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ ↑Hi_.f x = Hi_.α
Tactic:
have : x ∈ {x} := by
  exact Set.mem_singleton x
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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : x ∈ {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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : x ∈ {x}
⊢ ↑Hi_.f x = Hi_.α
Tactic:
rw [← hinterx, Set.mem_sInter] at this
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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : ∀ t ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, x ∈ t
⊢ ↑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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : ∀ t ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, x ∈ t
⊢ ↑Hi_.f x = Hi_.α
Tactic:
specialize this (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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : x ∈ frontier ↑Hi_
⊢ ↑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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : x ∈ frontier ↑Hi_
⊢ ↑Hi_.f x = Hi_.α
Tactic:
rw [frontierHalfspace_Hyperplane, Set.mem_setOf] at this
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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : ↑Hi_.f x = Hi_.α
⊢ ↑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_
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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : ↑Hi_.f x = Hi_.α
⊢ ↑Hi_.f x = Hi_.α
Tactic:
exact 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 : 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
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ x ∈ {x}
Tactic:
exact Set.mem_singleton x
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
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_.α
h : ↑Hi_.f x2 ≠ Hi_.α
⊢ ↑Hi_.f x2 ≤ Hi_.α
Tactic:
assumption
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 x1 < Hi_.α
⊢ False
Tactic:
rw [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, x1 + x_1 • (x2 - x1) = x
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < 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, x1 + x_1 • (x2 - x1) = x
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f (x1 + t • (x2 - 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f (x1 + t • (x2 - x1)) = 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ False
Tactic:
have : Hi_.f.1 x1 + t • Hi_.f.1 (x2 - x1) + (1-t) • Hi_.f.1 (x2 - x1) > 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
this : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) + (1 - t) • ↑Hi_.f (x2 - 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
this : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) + (1 - t) • ↑Hi_.f (x2 - x1) > 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
this : ↑Hi_.f 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
this : ↑Hi_.f x2 > 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) + (1 - t) • ↑Hi_.f (x2 - x1) > 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 x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ Hi_.α < Hi_.α + (1 - t) • ↑Hi_.f (x2 - x1)
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_.α + (1 - t) • ↑Hi_.f (x2 - x1)
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