internlm/Lean-Github huggingface dataset:
Theorem: Halfspace.val_eq'
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
⊢ (fun H_ => ↑(val p H_) ∩ ↑p) H_' = (fun H_ => Subtype.val '' H_) ↑H_'
Tactic:
apply subset_antisymm <;> intro x <;> rw [Set.mem_inter_iff, Set.mem_image]
Proof state after:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ x ∈ ↑(val p H_') ∧ x ∈ ↑p → ∃ x_1 ∈ ↑H_', ↑x_1 = x

case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ (∃ x_1 ∈ ↑H_', ↑x_1 = x) → x ∈ ↑(val p H_') ∧ x ∈ ↑p
Theorem: Halfspace.val_eq'
Proof state before:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ x ∈ ↑(val p H_') ∧ x ∈ ↑p → ∃ x_1 ∈ ↑H_', ↑x_1 = x
Tactic:
rintro ⟨ hxH_', hxp ⟩
Proof state after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ∃ x_1 ∈ ↑H_', ↑x_1 = x
Theorem: Halfspace.val_eq'
Proof state before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ∃ x_1 ∈ ↑H_', ↑x_1 = x
Tactic:
refine ⟨ ⟨ x, hxp ⟩, ?_, rfl ⟩
Proof state after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ { val := x, property := hxp } ∈ ↑H_'
Theorem: Halfspace.val_eq'
Proof state before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ { val := x, property := hxp } ∈ ↑H_'
Tactic:
rw [Halfspace_mem, ← (this ⟨ x, hxp ⟩), ← Halfspace.val_C p H_']
Proof state after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ↑(val p H_').f ↑{ val := x, property := hxp } ≤ (val p H_').α
Theorem: Halfspace.val_eq'
Proof state before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ↑(val p H_').f ↑{ val := x, property := hxp } ≤ (val p H_').α
Tactic:
exact hxH_'
Proof state after:
no goals
Theorem: Halfspace.val_eq'
Proof state before:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ (∃ x_1 ∈ ↑H_', ↑x_1 = x) → x ∈ ↑(val p H_') ∧ x ∈ ↑p
Tactic:
rintro ⟨ ⟨ x', hx'p ⟩, hx'H_', rfl ⟩
Proof state after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_') ∧ ↑{ val := x', property := hx'p } ∈ ↑p
Theorem: Halfspace.val_eq'
Proof state before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_') ∧ ↑{ val := x', property := hx'p } ∈ ↑p
Tactic:
refine ⟨ ?_, hx'p ⟩
Proof state after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Theorem: Halfspace.val_eq'
Proof state before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Tactic:
rw [Halfspace_mem, ← (this ⟨ x', hx'p ⟩), ← Halfspace.val_C p H_'] at hx'H_'
Proof state after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : ↑(val p H_').f ↑{ val := x', property := hx'p } ≤ (val p H_').α
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Theorem: Halfspace.val_eq'
Proof state before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : ↑(val p H_').f ↑{ val := x', property := hx'p } ≤ (val p H_').α
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Tactic:
exact hx'H_'
Proof state after:
no goals
Theorem: Convex_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ Convex ℝ (cutSpace H_)
Tactic:
apply convex_sInter
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ ∀ s ∈ SetLike.coe '' H_, Convex ℝ s
Theorem: Convex_cutSpace
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ ∀ s ∈ SetLike.coe '' H_, Convex ℝ s
Tactic:
rintro _ ⟨ Hi_, _, rfl ⟩
Proof state after:
case h.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ Convex ℝ ↑Hi_
Theorem: Convex_cutSpace
Proof state before:
case h.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ Convex ℝ ↑Hi_
Tactic:
exact Halfspace_convex Hi_
Proof state after:
no goals
Theorem: Closed_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ IsClosed (cutSpace H_)
Tactic:
apply isClosed_sInter
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ ∀ t ∈ SetLike.coe '' H_, IsClosed t
Theorem: Closed_cutSpace
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ ∀ t ∈ SetLike.coe '' H_, IsClosed t
Tactic:
rintro _ ⟨ Hi_, _, rfl ⟩
Proof state after:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ IsClosed ↑Hi_
Theorem: Closed_cutSpace
Proof state before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ IsClosed ↑Hi_
Tactic:
rw [Hi_.h]
Proof state after:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ IsClosed (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α})
Theorem: Closed_cutSpace
Proof state before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ IsClosed (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α})
Tactic:
apply IsClosed.preimage (Hi_.f.1.cont)
Proof state after:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ IsClosed {x | x ≤ Hi_.α}
Theorem: Closed_cutSpace
Proof state before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ IsClosed {x | x ≤ Hi_.α}
Tactic:
exact isClosed_Iic
Proof state after:
no goals
Theorem: mem_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ x ∈ cutSpace H_ ↔ ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Tactic:
constructor <;> intro h
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : x ∈ cutSpace H_
⊢ ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ cutSpace H_
Theorem: mem_cutSpace
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : x ∈ cutSpace H_
⊢ ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Tactic:
intro Hi HiH
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : x ∈ cutSpace H_
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_cutSpace
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : x ∈ cutSpace H_
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
unfold cutSpace at h
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : x ∈ ⋂₀ (SetLike.coe '' H_)
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_cutSpace
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : x ∈ ⋂₀ (SetLike.coe '' H_)
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rw [Set.mem_sInter] at h
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ t ∈ SetLike.coe '' H_, x ∈ t
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_cutSpace
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ t ∈ SetLike.coe '' H_, x ∈ t
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
specialize h Hi ⟨ Hi, HiH, rfl ⟩
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : x ∈ ↑Hi
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_cutSpace
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : x ∈ ↑Hi
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rw [Halfspace_mem] at h
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : ↑Hi.f x ≤ Hi.α
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_cutSpace
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : ↑Hi.f x ≤ Hi.α
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
exact h
Proof state after:
no goals
Theorem: mem_cutSpace
Proof state before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ cutSpace H_
Tactic:
unfold cutSpace
Proof state after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ ⋂₀ (SetLike.coe '' H_)
Theorem: mem_cutSpace
Proof state before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ ⋂₀ (SetLike.coe '' H_)
Tactic:
rw [Set.mem_sInter]
Proof state after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ ∀ t ∈ SetLike.coe '' H_, x ∈ t
Theorem: mem_cutSpace
Proof state before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ ∀ t ∈ SetLike.coe '' H_, x ∈ t
Tactic:
rintro _ ⟨ 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)
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x ∈ ↑Hi_
Theorem: mem_cutSpace
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x ∈ ↑Hi_
Tactic:
specialize h Hi_ hHi_
Proof state after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ x ∈ ↑Hi_
Theorem: mem_cutSpace
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ x ∈ ↑Hi_
Tactic:
rw [Halfspace_mem]
Proof state after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ ↑Hi_.f x ≤ Hi_.α
Theorem: mem_cutSpace
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ ↑Hi_.f x ≤ Hi_.α
Tactic:
exact h
Proof state after:
no goals
Theorem: empty_cutSpace
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
h : ∃ x, x ≠ 0
⊢ ∃ H_, cutSpace H_ = ∅
Tactic:
rcases h with ⟨ x, hx ⟩
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
⊢ ∃ H_, cutSpace H_ = ∅
Theorem: empty_cutSpace
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
⊢ ∃ H_, cutSpace H_ = ∅
Tactic:
let xhat := (norm x)⁻¹ • x
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
⊢ ∃ H_, cutSpace H_ = ∅
Theorem: empty_cutSpace
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
⊢ ∃ H_, cutSpace H_ = ∅
Tactic:
let fval : NormedSpace.Dual ℝ E := InnerProductSpace.toDualMap ℝ _ xhat
Proof state after:
case intro
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
⊢ ∃ H_, cutSpace H_ = ∅
Theorem: empty_cutSpace
Proof state before:
case intro
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
⊢ ∃ H_, cutSpace H_ = ∅
Tactic:
let f : {f : (NormedSpace.Dual ℝ E) // norm f = 1} := ⟨ fval , (by
  change norm (innerSL ℝ ((norm x)⁻¹ • x)) = 1
  have := @norm_smul_inv_norm ℝ _ E _ _ x hx
  rw [IsROrC.ofReal_real_eq_id, id_eq] at this
  rw [innerSL_apply_norm, this]
  done
) ⟩
Proof state after:
case intro
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 := ⋯ }
⊢ ∃ H_, cutSpace H_ = ∅
Theorem: empty_cutSpace
Proof state before:
case intro
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 := ⋯ }
⊢ ∃ H_, cutSpace H_ = ∅
Tactic:
refine ⟨ {Halfspace.mk f (-1), Halfspace.mk (-f) (-1)} , ?_ ⟩
Proof state after:
case intro
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 := ⋯ }
⊢ cutSpace {{ f := f, α := -1 }, { f := -f, α := -1 }} = ∅
Theorem: empty_cutSpace
Proof state before:
case intro
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 := ⋯ }
⊢ cutSpace {{ f := f, α := -1 }, { f := -f, α := -1 }} = ∅
Tactic:
ext x
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
⊢ x ∈ cutSpace {{ f := f, α := -1 }, { f := -f, α := -1 }} ↔ x ∈ ∅
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
⊢ x ∈ cutSpace {{ f := f, α := -1 }, { f := -f, α := -1 }} ↔ x ∈ ∅
Tactic:
rw [Set.mem_empty_iff_false, iff_false, mem_cutSpace]
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
⊢ ¬∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
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
⊢ ¬∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
Tactic:
intro h
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.α
⊢ 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.α
⊢ False
Tactic:
have h1 := h (Halfspace.mk f (-1)) (by simp)
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.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -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.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
⊢ False
Tactic:
have h2 := h (Halfspace.mk (-f) (-1)) (by simp)
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.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : ↑{ f := -f, α := -1 }.f x ≤ { f := -f, α := -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.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : ↑{ f := -f, α := -1 }.f x ≤ { f := -f, α := -1 }.α
⊢ False
Tactic:
rw [unitSphereDual_neg, ContinuousLinearMap.neg_apply, neg_le, neg_neg] at h2
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.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : 1 ≤ ↑f x
⊢ False