internlm/Lean-Github huggingface dataset:
Theorem: empty_cutSpace
Proof state before:
case intro.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : 1 ≤ ↑f x
⊢ False
Tactic:
change f.1 x ≤ -1 at h1
Proof state after:
case intro.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h2 : 1 ≤ ↑f x
h1 : ↑f x ≤ -1
⊢ False
Theorem: empty_cutSpace
Proof state before:
case intro.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h2 : 1 ≤ ↑f x
h1 : ↑f x ≤ -1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: empty_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖fval‖ = 1
Tactic:
change norm (innerSL ℝ ((norm x)⁻¹ • x)) = 1
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Theorem: empty_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
have := @norm_smul_inv_norm ℝ _ E _ _ x hx
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖(↑‖x‖)⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Theorem: empty_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖(↑‖x‖)⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
rw [IsROrC.ofReal_real_eq_id, id_eq] at this
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖‖x‖⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Theorem: empty_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖‖x‖⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
rw [innerSL_apply_norm, this]
Proof state after:
no goals
Theorem: empty_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
⊢ { f := f, α := -1 } ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}
Tactic:
simp
Proof state after:
no goals
Theorem: empty_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
⊢ { f := -f, α := -1 } ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}
Tactic:
simp
Proof state after:
no goals
Theorem: hyperplane_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ ∃ H_, cutSpace H_ = {x | ↑f x = c}
Tactic:
refine ⟨ {Halfspace.mk f c, Halfspace.mk (-f) (-c)}, ?_ ⟩
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ cutSpace {{ f := f, α := c }, { f := -f, α := -c }} = {x | ↑f x = c}
Theorem: hyperplane_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ cutSpace {{ f := f, α := c }, { f := -f, α := -c }} = {x | ↑f x = c}
Tactic:
ext x
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ x ∈ cutSpace {{ f := f, α := c }, { f := -f, α := -c }} ↔ x ∈ {x | ↑f x = c}
Theorem: hyperplane_cutSpace
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ x ∈ cutSpace {{ f := f, α := c }, { f := -f, α := -c }} ↔ x ∈ {x | ↑f x = c}
Tactic:
rw [mem_cutSpace, Set.mem_setOf]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ (∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α) ↔ ↑f x = c
Theorem: hyperplane_cutSpace
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ (∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α) ↔ ↑f x = c
Tactic:
constructor
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ (∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α) → ↑f x = c

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.α
Theorem: hyperplane_cutSpace
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ (∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α) → ↑f x = c
Tactic:
intro h
Proof state after:
case h.mp
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.α
⊢ ↑f x = c
Theorem: hyperplane_cutSpace
Proof state before:
case h.mp
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.α
⊢ ↑f x = c
Tactic:
have h1 := h (Halfspace.mk f c) (by simp)
Proof state after:
case h.mp
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 x = c
Theorem: hyperplane_cutSpace
Proof state before:
case h.mp
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 x = c
Tactic:
have h2 := h (Halfspace.mk (-f) (-c)) (by simp)
Proof state after:
case h.mp
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 }.α
h2 : ↑{ f := -f, α := -c }.f x ≤ { f := -f, α := -c }.α
⊢ ↑f x = c
Theorem: hyperplane_cutSpace
Proof state before:
case h.mp
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 }.α
h2 : ↑{ f := -f, α := -c }.f x ≤ { f := -f, α := -c }.α
⊢ ↑f x = c
Tactic:
rw [unitSphereDual_neg, ContinuousLinearMap.neg_apply, neg_le, neg_neg] at h2
Proof state after:
case h.mp
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 }.α
h2 : c ≤ ↑f x
⊢ ↑f x = c
Theorem: hyperplane_cutSpace
Proof state before:
case h.mp
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 }.α
h2 : c ≤ ↑f x
⊢ ↑f x = c
Tactic:
change f.1 x ≤ c at h1
Proof state after:
case h.mp
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.α
h2 : c ≤ ↑f x
h1 : ↑f x ≤ c
⊢ ↑f x = c
Theorem: hyperplane_cutSpace
Proof state before:
case h.mp
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.α
h2 : c ≤ ↑f x
h1 : ↑f x ≤ c
⊢ ↑f x = c
Tactic:
exact le_antisymm h1 h2
Proof state after:
no goals
Theorem: hyperplane_cutSpace
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.α
⊢ { f := f, α := c } ∈ {{ f := f, α := c }, { f := -f, α := -c }}
Tactic:
simp
Proof state after:
no goals
Theorem: hyperplane_cutSpace
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_cutSpace
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_cutSpace
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_cutSpace
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_cutSpace
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_cutSpace
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_cutSpace
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_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
⊢ cutSpace (H_1 ∪ H_2) = cutSpace H_1 ∩ cutSpace H_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)
x : E
⊢ x ∈ cutSpace (H_1 ∪ H_2) ↔ x ∈ cutSpace H_1 ∩ cutSpace H_2
Theorem: inter_cutSpace
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
x : E
⊢ x ∈ cutSpace (H_1 ∪ H_2) ↔ x ∈ cutSpace H_1 ∩ cutSpace H_2
Tactic:
rw [mem_cutSpace, Set.mem_inter_iff, mem_cutSpace, mem_cutSpace]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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_cutSpace
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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)
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)
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_cutSpace
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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)
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_cutSpace
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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_cutSpace
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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)
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_cutSpace
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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)
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_cutSpace
Proof state before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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)
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)
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_cutSpace
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)
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_cutSpace
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)
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: orthoHyperplane.Finite
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
⊢ Set.Finite (orthoHyperplane x)
Tactic:
unfold orthoHyperplane
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
⊢ Set.Finite {{ f := pointDualLin x, α := 0 }, { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }}
Theorem: orthoHyperplane.Finite
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
⊢ Set.Finite {{ f := pointDualLin x, α := 0 }, { f := pointDualLin { val := -↑x, property := ⋯ }, α := 0 }}
Tactic:
simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, and_true, Set.finite_singleton, Set.Finite.insert]
Proof state after:
no goals
Theorem: orthoHyperplane_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
⊢ ∀ (y : E), y ∈ cutSpace (orthoHyperplane x) ↔ ⟪↑x, y⟫_ℝ = 0
Tactic:
intro y
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ y ∈ cutSpace (orthoHyperplane x) ↔ ⟪↑x, y⟫_ℝ = 0
Theorem: orthoHyperplane_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ y ∈ cutSpace (orthoHyperplane x) ↔ ⟪↑x, y⟫_ℝ = 0
Tactic:
rw [mem_cutSpace]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ (∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α) ↔ ⟪↑x, y⟫_ℝ = 0
Theorem: orthoHyperplane_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ (∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α) ↔ ⟪↑x, y⟫_ℝ = 0
Tactic:
constructor
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ (∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α) → ⟪↑x, y⟫_ℝ = 0

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ ⟪↑x, y⟫_ℝ = 0 → ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
Theorem: orthoHyperplane_mem
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
⊢ (∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α) → ⟪↑x, y⟫_ℝ = 0
Tactic:
intro h
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
⊢ ⟪↑x, y⟫_ℝ = 0
Theorem: orthoHyperplane_mem
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
have h1 := h (Halfspace.mk (pointDualLin x) 0)
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 :
  { f := pointDualLin x, α := 0 } ∈ orthoHyperplane x →
    ↑{ f := pointDualLin x, α := 0 }.f y ≤ { f := pointDualLin x, α := 0 }.α
⊢ ⟪↑x, y⟫_ℝ = 0
Theorem: orthoHyperplane_mem
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 :
  { f := pointDualLin x, α := 0 } ∈ orthoHyperplane x →
    ↑{ f := pointDualLin x, α := 0 }.f y ≤ { f := pointDualLin x, α := 0 }.α
⊢ ⟪↑x, y⟫_ℝ = 0
Tactic:
simp only [pointDualLin, ne_eq, map_inv₀, IsROrC.conj_to_real, orthoHyperplane, Set.mem_singleton_iff,
  Halfspace.mk.injEq, and_true, Set.mem_insert_iff, true_or, forall_true_left, InnerProductSpace.toDual_apply,
  inner_smul_left] at h1
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : { x // x ≠ 0 }
y : E
h : ∀ Hi ∈ orthoHyperplane x, ↑Hi.f y ≤ Hi.α
h1 : ‖↑x‖⁻¹ * ⟪↑x, y⟫_ℝ ≤ 0
⊢ ⟪↑x, y⟫_ℝ = 0