Theorem: Vpolytope_of_Vpolytope_inter_cutSpace_fin (src/MainTheorem.lean)

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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
rcases Hpolytope_of_Vpolytope_interior _ hVinterior with ⟨ H_', hH_', hHV ⟩
State after:
case intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_

State before:
case intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
have hH_inter := inter_Hpolytope H_' H_ hH_' hH_
State after:
case intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_

State before:
case intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
have : IsCompact (Vpolytope hS ∩ Hpolytope hH_) := (Compact_Vpolytope hS).inter_right (Closed_cutSpace H_)
State after:
case intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Vpolytope hS ∩ Hpolytope hH_)
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_

State before:
case intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Vpolytope hS ∩ Hpolytope hH_)
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
rw [← hHV, ← hH_inter] at this
State after:
case intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_

State before:
case intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
rcases Vpolytope_of_Hpolytope (hH_'.union hH_) this with ⟨ S', hS', hSV ⟩
State after:
case intro.intro.intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
S' : Set E
hS' : Set.Finite S'
hSV : Hpolytope ⋯ = Vpolytope hS'
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_

State before:
case intro.intro.intro.intro
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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
S' : Set E
hS' : Set.Finite S'
hSV : Hpolytope ⋯ = Vpolytope hS'
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
exact ⟨ S', hS', by rw [← hSV, ← hHV, ← hH_inter] ⟩
State after:
no goals

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✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
S' : Set E
hS' : Set.Finite S'
hSV : Hpolytope ⋯ = Vpolytope hS'
⊢ Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
rw [← hSV, ← hHV, ← hH_inter]
State after:
no goals