internlm/Lean-Github huggingface dataset:
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_2.hs
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ S - {s} ⊆ {x | x ∈ AffineSubspace.direction SpanS}
Tactic:
exact AffineSubspace.direction_subset_subset (subset_affineSpan ℝ S)
  (subset_trans (Set.singleton_subset_iff.mpr hs) (subset_affineSpan ℝ S))
Proof state after:
no goals
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_2.hf
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Function.Injective (LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS))).toFun
Tactic:
(try rw [AffineMap.toFun_eq_coe])
Proof state after:
case refine_2.hf
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Function.Injective ⇑(LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS)))
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_2.hf
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Function.Injective (LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS))).toFun
Tactic:
try rw [AffineMap.toFun_eq_coe]
Proof state after:
case refine_2.hf
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Function.Injective ⇑(LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS)))
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_2.hf
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Function.Injective (LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS))).toFun
Tactic:
rw [AffineMap.toFun_eq_coe]
Proof state after:
case refine_2.hf
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Function.Injective ⇑(LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS)))
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_2.hs
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ S - {s} ⊆ Set.range ⇑(LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS)))
Tactic:
rw [LinearMap.coe_toAffineMap, Submodule.coeSubtype]
Proof state after:
case refine_2.hs
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))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ S - {s} ⊆ Set.range Subtype.val
Theorem: MainTheoremOfPolytopes
Proof state before:
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 : Hpolytope hH''1 = 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
⊢ Nontrivial ↥(AffineSubspace.direction SpanS)
Tactic:
apply AffineSubspace.direction_nontrivial_of_nontrivial
Proof state after:
case 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 : Hpolytope hH''1 = 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
⊢ Nontrivial ↥SpanS
Theorem: MainTheoremOfPolytopes
Proof state before:
case 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 : Hpolytope hH''1 = 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
⊢ Nontrivial ↥SpanS
Tactic:
exact affineSpan_nontrivial ℝ (Set.nontrivial_coe_sort.mpr hSnontrivial)
Proof state after:
no goals
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs
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 : Hpolytope hH''1 = 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)
⊢ Set.Nonempty (SetLike.coe '' H_'1)
Tactic:
(apply Set.Nonempty.image)
Proof state after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.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 : Hpolytope hH''1 = 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)
⊢ Set.Nonempty H_'1
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs
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 : Hpolytope hH''1 = 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)
⊢ Set.Nonempty (SetLike.coe '' H_'1)
Tactic:
apply Set.Nonempty.image
Proof state after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.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 : Hpolytope hH''1 = 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)
⊢ Set.Nonempty H_'1
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.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 : Hpolytope hH''1 = 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)
⊢ Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)
Tactic:
try apply Set.Nonempty.image
Proof state after:
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 : Hpolytope hH''1 = 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)
⊢ Set.Nonempty H_''1