internlm/Lean-Github huggingface dataset:
Theorem: Hpolytope_of_Vpolytope_0interior
Proof 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, _ ⟩
Proof 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
Theorem: Hpolytope_of_Vpolytope_0interior
Proof 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_', ?_ ⟩
Proof 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
Theorem: Hpolytope_of_Vpolytope_0interior
Proof 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)]
Proof state after:
no goals
Theorem: Hpolytope_of_Vpolytope_0interior
Proof 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)]
Proof 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)
Theorem: Hpolytope_of_Vpolytope_0interior
Proof 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
Proof state after:
no goals
Theorem: translationHomeo
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x y : E
⊢ (fun x_1 => x_1 + -x) ((fun x_1 => x_1 + x) y) = y
Tactic:
simp
Proof state after:
no goals
Theorem: translationHomeo
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x y : E
⊢ (fun x_1 => x_1 + x) ((fun x_1 => x_1 + -x) y) = y
Tactic:
simp
Proof state after:
no goals
Theorem: translationHomeo
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ Continuous { toFun := fun x_1 => x_1 + x, invFun := fun x_1 => x_1 + -x, left_inv := ⋯, right_inv := ⋯ }.toFun
Tactic:
continuity
Proof state after:
no goals
Theorem: translationHomeo
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ Continuous { toFun := fun x_1 => x_1 + x, invFun := fun x_1 => x_1 + -x, left_inv := ⋯, right_inv := ⋯ }.invFun
Tactic:
continuity
Proof state after:
no goals
Theorem: translationHomeo.toFun.def
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ ⇑(translationHomeo x) = fun x_1 => x_1 + x
Tactic:
unfold translationHomeo
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ ⇑{ toEquiv := { toFun := fun x_1 => x_1 + x, invFun := fun x_1 => x_1 + -x, left_inv := ⋯, right_inv := ⋯ },
        continuous_toFun := ⋯, continuous_invFun := ⋯ } =
    fun x_1 => x_1 + x
Theorem: translationHomeo.toFun.def
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ ⇑{ toEquiv := { toFun := fun x_1 => x_1 + x, invFun := fun x_1 => x_1 + -x, left_inv := ⋯, right_inv := ⋯ },
        continuous_toFun := ⋯, continuous_invFun := ⋯ } =
    fun x_1 => x_1 + x
Tactic:
simp
Proof state after:
no goals
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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}
Proof 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
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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))
Proof 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
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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
Proof 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
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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 ⟩
Proof 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
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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_'
Proof 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
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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 _
Proof 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
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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_, ?_ ⟩
Proof 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
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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
Proof 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
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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]
Proof state after:
no goals
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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))
Proof state after:
no goals
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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, ]
Proof 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)
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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)
Proof 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)
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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
Proof 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)
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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]
Proof 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)
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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
Proof 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)
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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]
Proof 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)
Theorem: Hpolytope_of_Vpolytope_interior
Proof 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
Proof state after:
no goals