internlm/Lean-Github huggingface dataset:
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝¹ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this✝ : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
S' : Set ↥(AffineSubspace.direction SpanS)
hx : x ∈ interior ((convexHull ℝ) S')
hS'Fin : Set.Finite S'
hS'eq : (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
hS' : Set.Nonempty (interior (Vpolytope hS'Fin))
H_''1 : Set (Halfspace ↥(AffineSubspace.direction SpanS))
hH''1 : Set.Finite H_''1
hHV : Set.univ = Vpolytope hS'Fin
H_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False
Tactic:
exact IsCompact.ne_univ (Compact_Vpolytope hS'Fin) hHV.symm
Proof state after:
no goals
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inr
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : ¬Set.Nontrivial S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rw [Set.not_nontrivial_iff] at hStrivial
Proof state after:
case left.inr
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inr
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
exact Hpolytope_of_Vpolytope_subsingleton _ hStrivial
Proof state after:
no goals
Theorem: MainTheoremOfPolytopes
Proof state before:
case right
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
⊢ ∀ {H_ : Set (Halfspace E)} (hH_ : Set.Finite H_),
    IsCompact (Hpolytope hH_) → ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Tactic:
exact Vpolytope_of_Hpolytope
Proof state after:
no goals
Theorem: Closed_Vpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set E
hS : Set.Finite S
⊢ IsClosed (Vpolytope hS)
Tactic:
exact Set.Finite.isClosed_convexHull hS
Proof state after:
no goals
Theorem: Convex_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ Convex ℝ (Hpolytope hH_)
Tactic:
apply convex_sInter
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ ∀ s ∈ SetLike.coe '' H_, Convex ℝ s
Theorem: Convex_Hpolytope
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ ∀ 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)
hH_ : Set.Finite H_
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ Convex ℝ ↑Hi_
Theorem: Convex_Hpolytope
Proof state before:
case h.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ Convex ℝ ↑Hi_
Tactic:
exact Halfspace_convex Hi_
Proof state after:
no goals
Theorem: Closed_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
⊢ IsClosed (Hpolytope hH_)
Tactic:
apply isClosed_sInter
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
⊢ ∀ t ∈ SetLike.coe '' H, IsClosed t
Theorem: Closed_Hpolytope
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
⊢ ∀ 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)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed ↑Hi_
Theorem: Closed_Hpolytope
Proof state before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
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)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α})
Theorem: Closed_Hpolytope
Proof state before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
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)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed {x | x ≤ Hi_.α}
Theorem: Closed_Hpolytope
Proof state before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed {x | x ≤ Hi_.α}
Tactic:
exact isClosed_Iic
Proof state after:
no goals
Theorem: Hpolytope_same
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_1 hH_2 : Set.Finite H_
⊢ Hpolytope hH_1 = Hpolytope hH_2
Tactic:
unfold Hpolytope
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_1 hH_2 : Set.Finite H_
⊢ ⋂₀ (SetLike.coe '' H_) = ⋂₀ (SetLike.coe '' H_)
Theorem: Hpolytope_same
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_1 hH_2 : Set.Finite H_
⊢ ⋂₀ (SetLike.coe '' H_) = ⋂₀ (SetLike.coe '' H_)
Tactic:
rfl
Proof state after:
no goals
Theorem: mem_Hpolytope
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 ∈ Hpolytope hH_ ↔ ∀ 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)
hH_ : Set.Finite H_
x : E
h : x ∈ Hpolytope hH_
⊢ ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ Hpolytope hH_
Theorem: mem_Hpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ Hpolytope hH_
⊢ ∀ 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)
hH_ : Set.Finite H_
x : E
h : x ∈ Hpolytope hH_
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_Hpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ Hpolytope hH_
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
unfold Hpolytope at h
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ ⋂₀ (SetLike.coe '' H_)
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_Hpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
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)
hH_ : Set.Finite H_
x : E
h : ∀ t ∈ SetLike.coe '' H_, x ∈ t
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_Hpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
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)
hH_ : Set.Finite H_
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : x ∈ ↑Hi
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_Hpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
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)
hH_ : Set.Finite H_
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : ↑Hi.f x ≤ Hi.α
⊢ ↑Hi.f x ≤ Hi.α
Theorem: mem_Hpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
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_Hpolytope
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
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ Hpolytope hH_
Tactic:
unfold Hpolytope
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
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ ⋂₀ (SetLike.coe '' H_)
Theorem: mem_Hpolytope
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
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)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ ∀ t ∈ SetLike.coe '' H_, x ∈ t
Theorem: mem_Hpolytope
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
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)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x ∈ ↑Hi_
Theorem: mem_Hpolytope
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
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)
hH_ : Set.Finite H_
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ x ∈ ↑Hi_
Theorem: mem_Hpolytope
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
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)
hH_ : Set.Finite H_
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ ↑Hi_.f x ≤ Hi_.α
Theorem: mem_Hpolytope
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
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_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
have h := exists_ne (0:E)
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
h : ∃ y, y ≠ 0
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Theorem: empty_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
h : ∃ y, y ≠ 0
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
rcases h with ⟨ x, hx ⟩
Proof state after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Theorem: empty_Hpolytope
Proof state before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
let xhat := (norm x)⁻¹ • x
Proof state after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Theorem: empty_Hpolytope
Proof state before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
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
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Theorem: empty_Hpolytope
Proof state before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
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
inst✝ : Nontrivial 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_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Theorem: empty_Hpolytope
Proof state before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
refine ⟨ {Halfspace.mk f (-1), Halfspace.mk (-f) (-1)} ,
  (by simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, Set.finite_singleton, Set.Finite.insert]) , ?_ ⟩
Proof state after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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 := ⋯ }
⊢ Hpolytope ⋯ = ∅
Theorem: empty_Hpolytope
Proof state before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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 := ⋯ }
⊢ Hpolytope ⋯ = ∅
Tactic:
ext x
Proof state after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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 ∈ Hpolytope ⋯ ↔ x ∈ ∅
Theorem: empty_Hpolytope
Proof state before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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 ∈ Hpolytope ⋯ ↔ x ∈ ∅
Tactic:
rw [Set.mem_empty_iff_false, iff_false, mem_Hpolytope]
Proof state after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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_Hpolytope
Proof state before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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
inst✝ : Nontrivial 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_Hpolytope
Proof state before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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
inst✝ : Nontrivial 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_Hpolytope
Proof state before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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
inst✝ : Nontrivial 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_Hpolytope
Proof state before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial 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
inst✝ : Nontrivial 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