internlm/Lean-Github huggingface dataset:
Theorem: hyperplane_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
⊢ { f := -f, α := -c } ∈ {{ f := f, α := c }, { f := -f, α := -c }}
Tactic:
simp
Proof state after:
no goals
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ ↑f x = c → ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
Tactic:
intro h Hi hHi
Proof state after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
Hi : Halfspace E
hHi : Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}
⊢ ↑Hi.f x ≤ Hi.α
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
Hi : Halfspace E
hHi : Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, Set.mem_insert_iff] at hHi
Proof state after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
Hi : Halfspace E
hHi : Hi = { f := f, α := c } ∨ Hi = { f := -f, α := -c }
⊢ ↑Hi.f x ≤ Hi.α
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
Hi : Halfspace E
hHi : Hi = { f := f, α := c } ∨ Hi = { f := -f, α := -c }
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rcases hHi with rfl | rfl
Proof state after:
case h.mpr.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α

case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ ↑{ f := -f, α := -c }.f x ≤ { f := -f, α := -c }.α
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mpr.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
Tactic:
exact le_of_eq h
Proof state after:
no goals
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ ↑{ f := -f, α := -c }.f x ≤ { f := -f, α := -c }.α
Tactic:
rw [unitSphereDual_neg, ContinuousLinearMap.neg_apply, neg_le, neg_neg]
Proof state after:
case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ c ≤ ↑f x
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ c ≤ ↑f x
Tactic:
exact le_of_eq h.symm
Proof state after:
no goals
Theorem: inter_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
⊢ Hpolytope ⋯ = Hpolytope hH_1 ∩ Hpolytope hH_2
Tactic:
ext x
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ Hpolytope hH_1 ∩ Hpolytope hH_2
Theorem: inter_Hpolytope
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ Hpolytope hH_1 ∩ Hpolytope hH_2
Tactic:
rw [mem_Hpolytope, Set.mem_inter_iff, mem_Hpolytope, mem_Hpolytope]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ (∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α) ↔ (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Theorem: inter_Hpolytope
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ (∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α) ↔ (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Tactic:
constructor
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ (∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α) → (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ ((∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α) → ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
Theorem: inter_Hpolytope
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ (∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α) → (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Tactic:
intro h
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
⊢ (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Theorem: inter_Hpolytope
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
⊢ (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Tactic:
constructor <;> intro Hi_ hH_ <;> exact h Hi_ (by simp only [Set.mem_union, hH_, true_or, or_true])
Proof state after:
no goals
Theorem: inter_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
Hi_ : Halfspace E
hH_ : Hi_ ∈ H_2
⊢ Hi_ ∈ H_1 ∪ H_2
Tactic:
simp only [Set.mem_union, hH_, true_or, or_true]
Proof state after:
no goals
Theorem: inter_Hpolytope
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ ((∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α) → ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
Tactic:
intro h Hi hHi
Proof state after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1 ∪ H_2
⊢ ↑Hi.f x ≤ Hi.α
Theorem: inter_Hpolytope
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1 ∪ H_2
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rw [Set.mem_union] at hHi
Proof state after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1 ∨ Hi ∈ H_2
⊢ ↑Hi.f x ≤ Hi.α
Theorem: inter_Hpolytope
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1 ∨ Hi ∈ H_2
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rcases hHi with hHi | hHi
Proof state after:
case h.mpr.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1
⊢ ↑Hi.f x ≤ Hi.α

case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_2
⊢ ↑Hi.f x ≤ Hi.α
Theorem: inter_Hpolytope
Proof state before:
case h.mpr.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
exact h.1 Hi hHi
Proof state after:
no goals
Theorem: inter_Hpolytope
Proof state before:
case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_2
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
exact h.2 Hi hHi
Proof state after:
no goals
Theorem: Vpolytope_translation
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set E
hS : Set.Finite S
x : E
⊢ Vpolytope ⋯ = Vpolytope hS + {x}
Tactic:
rw [Vpolytope, convexHull_add, convexHull_singleton]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set E
hS : Set.Finite S
x : E
⊢ (convexHull ℝ) S + {x} = Vpolytope hS + {x}
Theorem: Vpolytope_translation
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set E
hS : Set.Finite S
x : E
⊢ (convexHull ℝ) S + {x} = Vpolytope hS + {x}
Tactic:
rfl
Proof state after:
no goals
Theorem: Hpolytope_translation
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
⊢ Hpolytope ⋯ = Hpolytope hH_ + {x}
Tactic:
rw [Hpolytope, Hpolytope, Set.sInter_image, Set.sInter_image]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
⊢ ⋂ x_1 ∈ Halfspace_translation x '' H_, ↑x_1 = (⋂ x ∈ H_, ↑x) + {x}
Theorem: Hpolytope_translation
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
⊢ ⋂ x_1 ∈ Halfspace_translation x '' H_, ↑x_1 = (⋂ x ∈ H_, ↑x) + {x}
Tactic:
ext y
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ y ∈ ⋂ x_1 ∈ Halfspace_translation x '' H_, ↑x_1 ↔ y ∈ (⋂ x ∈ H_, ↑x) + {x}
Theorem: Hpolytope_translation
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ y ∈ ⋂ x_1 ∈ Halfspace_translation x '' H_, ↑x_1 ↔ y ∈ (⋂ x ∈ H_, ↑x) + {x}
Tactic:
rw [Set.mem_iInter, Set.add_singleton]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ (i : Halfspace E), y ∈ ⋂ (_ : i ∈ Halfspace_translation x '' H_), ↑i) ↔ y ∈ (fun x_1 => x_1 + x) '' ⋂ x ∈ H_, ↑x
Theorem: Hpolytope_translation
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ (i : Halfspace E), y ∈ ⋂ (_ : i ∈ Halfspace_translation x '' H_), ↑i) ↔ y ∈ (fun x_1 => x_1 + x) '' ⋂ x ∈ H_, ↑x
Tactic:
simp only [Set.mem_iInter, SetLike.mem_coe, Set.image_add_right, Set.mem_preimage]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ Halfspace_translation x '' H_, y ∈ i) ↔ ∀ i ∈ H_, y + -x ∈ i
Theorem: Hpolytope_translation
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ Halfspace_translation x '' H_, y ∈ i) ↔ ∀ i ∈ H_, y + -x ∈ i
Tactic:
constructor
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ Halfspace_translation x '' H_, y ∈ i) → ∀ i ∈ H_, y + -x ∈ i

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ H_, y + -x ∈ i) → ∀ i ∈ Halfspace_translation x '' H_, y ∈ i
Theorem: Hpolytope_translation
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ Halfspace_translation x '' H_, y ∈ i) → ∀ i ∈ H_, y + -x ∈ i
Tactic:
intro h Hi_ hHi_
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ Halfspace_translation x '' H_, y ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ y + -x ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ Halfspace_translation x '' H_, y ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ y + -x ∈ Hi_
Tactic:
specialize h (Halfspace_translation x Hi_) (Set.mem_image_of_mem _ hHi_)
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : y ∈ Halfspace_translation x Hi_
⊢ y + -x ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : y ∈ Halfspace_translation x Hi_
⊢ y + -x ∈ Hi_
Tactic:
rw [← SetLike.mem_coe, mem_Halfspace_translation, sub_eq_add_neg] at h
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : y + -x ∈ ↑Hi_
⊢ y + -x ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : y + -x ∈ ↑Hi_
⊢ y + -x ∈ Hi_
Tactic:
exact h
Proof state after:
no goals
Theorem: Hpolytope_translation
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ H_, y + -x ∈ i) → ∀ i ∈ Halfspace_translation x '' H_, y ∈ i
Tactic:
intro h Hi_ hHi_
Proof state after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
⊢ y ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
⊢ y ∈ Hi_
Tactic:
specialize h (Halfspace_translation (-x) Hi_) (?_)
Proof state after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
⊢ Halfspace_translation (-x) Hi_ ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
⊢ Halfspace_translation (-x) Hi_ ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
rw [Set.mem_image] at hHi_
Proof state after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : ∃ x_1 ∈ H_, Halfspace_translation x x_1 = Hi_
⊢ Halfspace_translation (-x) Hi_ ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : ∃ x_1 ∈ H_, Halfspace_translation x x_1 = Hi_
⊢ Halfspace_translation (-x) Hi_ ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
rcases hHi_ with ⟨ Hi_', hHi_', rfl ⟩
Proof state after:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
have : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_':= by
  rw [SetLike.ext_iff]
  intro z
  rw [← SetLike.mem_coe, ← SetLike.mem_coe, mem_Halfspace_translation, mem_Halfspace_translation,
    sub_neg_eq_add, add_sub_cancel]
  done
Proof state after:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
this : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
this : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
rw [this]
Proof state after:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
this : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
⊢ Hi_' ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Theorem: Hpolytope_translation
Proof state before:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
this : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
⊢ Hi_' ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
assumption
Proof state after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_