Theorem: Hpolytope_of_Vpolytope_0interior (src/MainTheorem.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases DualOfVpolytope_compactHpolytope hS hV0 with ⟨ H_, hH_, hH_eq, hH_cpt ⟩
State after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases Vpolytope_of_Hpolytope hH_ hH_cpt with ⟨ S', hS', hS'eq ⟩
State after:
case intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have : 0 ∈ interior (Vpolytope hS') := by
  rw [←hS'eq, hH_eq, compact_polarDual_iff (Closed_Vpolytope hS)]
  exact Compact_Vpolytope hS
State after:
case intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
this : 0 ∈ interior (Vpolytope hS')
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
this : 0 ∈ interior (Vpolytope hS')
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases DualOfVpolytope_compactHpolytope hS' this with ⟨ H_', hH_', hH_'eq, _ ⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = polarDual (Vpolytope hS')
right✝ : IsCompact (Hpolytope hH_')
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = polarDual (Vpolytope hS')
right✝ : IsCompact (Hpolytope hH_')
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
refine ⟨ H_', hH_', ?_ ⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = polarDual (Vpolytope hS')
right✝ : IsCompact (Hpolytope hH_')
⊢ Hpolytope hH_' = Vpolytope hS

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = polarDual (Vpolytope hS')
right✝ : IsCompact (Hpolytope hH_')
⊢ Hpolytope hH_' = Vpolytope hS
Tactic:
rw [hH_'eq, ←hS'eq, hH_eq, doublePolarDual_self (Closed_Vpolytope hS) (Convex_Vpolytope hS) (interior_subset hV0)]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
⊢ 0 ∈ interior (Vpolytope hS')
Tactic:
rw [←hS'eq, hH_eq, compact_polarDual_iff (Closed_Vpolytope hS)]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
⊢ IsCompact (Vpolytope hS)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
⊢ IsCompact (Vpolytope hS)
Tactic:
exact Compact_Vpolytope hS
State after:
no goals