Theorem: Hpolytope_of_Vpolytope_interior (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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
let S' := S + {-hVinteriorNonempty.some}
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = 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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have hS' : S'.Finite := by exact (hS.translation (-hVinteriorNonempty.some))
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = 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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have : 0 ∈ interior (Vpolytope hS') := by
  rw [Vpolytope_translation hS, Set.add_singleton, ]
  have := @Homeomorph.image_interior _ _ _ _ (translationHomeo (-hVinteriorNonempty.some)) (Vpolytope hS)
  rw [translationHomeo.toFun.def] at this
  rw [← this]; clear this
  rw [← Set.add_singleton, Set.mem_translation, zero_sub,  neg_neg]
  exact hVinteriorNonempty.some_mem
  done
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = 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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases Hpolytope_of_Vpolytope_0interior hS' this with ⟨ H_', hH_', hH_'eq ⟩
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
let H_ := (Halfspace_translation hVinteriorNonempty.some) '' H_'
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
H_ : Set (Halfspace E) := Halfspace_translation (Set.Nonempty.some hVinteriorNonempty) '' H_'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
H_ : Set (Halfspace E) := Halfspace_translation (Set.Nonempty.some hVinteriorNonempty) '' H_'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have hH_ : H_.Finite := hH_'.image _
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
H_ : Set (Halfspace E) := Halfspace_translation (Set.Nonempty.some hVinteriorNonempty) '' H_'
hH_ : Set.Finite H_
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
H_ : Set (Halfspace E) := Halfspace_translation (Set.Nonempty.some hVinteriorNonempty) '' H_'
hH_ : Set.Finite H_
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
refine ⟨ H_, hH_, ?_ ⟩
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
H_ : Set (Halfspace E) := Halfspace_translation (Set.Nonempty.some hVinteriorNonempty) '' H_'
hH_ : Set.Finite H_
⊢ Hpolytope hH_ = Vpolytope hS

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
H_ : Set (Halfspace E) := Halfspace_translation (Set.Nonempty.some hVinteriorNonempty) '' H_'
hH_ : Set.Finite H_
⊢ Hpolytope hH_ = Vpolytope hS
Tactic:
ext x
State after:
case intro.intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
H_ : Set (Halfspace E) := Halfspace_translation (Set.Nonempty.some hVinteriorNonempty) '' H_'
hH_ : Set.Finite H_
x : E
⊢ x ∈ Hpolytope hH_ ↔ x ∈ Vpolytope hS

State before:
case intro.intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this : 0 ∈ interior (Vpolytope hS')
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hH_'eq : Hpolytope hH_' = Vpolytope hS'
H_ : Set (Halfspace E) := Halfspace_translation (Set.Nonempty.some hVinteriorNonempty) '' H_'
hH_ : Set.Finite H_
x : E
⊢ x ∈ Hpolytope hH_ ↔ x ∈ Vpolytope hS
Tactic:
rw [Hpolytope_translation, hH_'eq, Vpolytope_translation hS, ← Set.sub_eq_neg_add,
  Set.neg_add_cancel_right' hVinteriorNonempty.some]
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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
⊢ Set.Finite S'
Tactic:
exact (hS.translation (-hVinteriorNonempty.some))
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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ 0 ∈ interior (Vpolytope hS')
Tactic:
rw [Vpolytope_translation hS, Set.add_singleton, ]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ 0 ∈ interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' 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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ 0 ∈ interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' Vpolytope hS)
Tactic:
have := @Homeomorph.image_interior _ _ _ _ (translationHomeo (-hVinteriorNonempty.some)) (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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this :
  ⇑(translationHomeo (-Set.Nonempty.some hVinteriorNonempty)) '' interior (Vpolytope hS) =
    interior (⇑(translationHomeo (-Set.Nonempty.some hVinteriorNonempty)) '' Vpolytope hS)
⊢ 0 ∈ interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' 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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this :
  ⇑(translationHomeo (-Set.Nonempty.some hVinteriorNonempty)) '' interior (Vpolytope hS) =
    interior (⇑(translationHomeo (-Set.Nonempty.some hVinteriorNonempty)) '' Vpolytope hS)
⊢ 0 ∈ interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' Vpolytope hS)
Tactic:
rw [translationHomeo.toFun.def] at this
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this :
  (fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' interior (Vpolytope hS) =
    interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' Vpolytope hS)
⊢ 0 ∈ interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' 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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this :
  (fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' interior (Vpolytope hS) =
    interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' Vpolytope hS)
⊢ 0 ∈ interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' Vpolytope hS)
Tactic:
rw [← this]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this :
  (fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' interior (Vpolytope hS) =
    interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' Vpolytope hS)
⊢ 0 ∈ (fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' interior (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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
this :
  (fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' interior (Vpolytope hS) =
    interior ((fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' Vpolytope hS)
⊢ 0 ∈ (fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' interior (Vpolytope hS)
Tactic:
clear this
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ 0 ∈ (fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' interior (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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ 0 ∈ (fun x => x + -Set.Nonempty.some hVinteriorNonempty) '' interior (Vpolytope hS)
Tactic:
rw [← Set.add_singleton, Set.mem_translation, zero_sub,  neg_neg]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ Set.Nonempty.some hVinteriorNonempty ∈ interior (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
hVinteriorNonempty : Set.Nonempty (interior (Vpolytope hS))
S' : Set E := S + {-Set.Nonempty.some hVinteriorNonempty}
hS' : Set.Finite S'
⊢ Set.Nonempty.some hVinteriorNonempty ∈ interior (Vpolytope hS)
Tactic:
exact hVinteriorNonempty.some_mem
State after:
no goals