internlm/Lean-Github huggingface dataset:
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hExHFinite

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ IsClosed ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)))
Tactic:
rfl
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ IsClosed ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
hExHFinite : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
this : closure ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_))) = Hpolytope hH_
⊢ IsClosed ((convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)))
Tactic:
exact Closed_Vpolytope hExHFinite
Proof state after:
no goals
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
have := ExtremePointsofHpolytope hH_
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
let g : E ↪ Set E :=
  ⟨ fun x : E => Set.singleton x, Set.singleton_injective ⟩
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
rcases Set.Finite.exists_finset_coe hH_ with ⟨ Hfin, hHfin ⟩
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
let PHfin := Hfin.powerset
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
let PH := Finset.toSet '' PHfin.toSet
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
have hPH : PH.Finite := PHfin.finite_toSet.image _
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
have hfPH : (f '' PH).Finite := hPH.image f
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
have hgExFin : Set.Finite <| g '' (Set.extremePoints ℝ (Hpolytope hH_)) := Set.Finite.subset hfPH hgfPH
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
have := hgExFin.preimage_embedding g
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this✝ :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
this : Set.Finite (⇑g ⁻¹' (⇑g '' Set.extremePoints ℝ (Hpolytope hH_)))
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this✝ :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
this : Set.Finite (⇑g ⁻¹' (⇑g '' Set.extremePoints ℝ (Hpolytope hH_)))
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
Tactic:
rw [Function.Injective.preimage_image] at this
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this✝ :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
this : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))

case intro.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this✝ :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
this : Set.Finite (⇑g ⁻¹' (⇑g '' Set.extremePoints ℝ (Hpolytope hH_)))
⊢ Function.Injective ⇑g
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this✝ :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
this : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))
⊢ Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))

case intro.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this✝ :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
this : Set.Finite (⇑g ⁻¹' (⇑g '' Set.extremePoints ℝ (Hpolytope hH_)))
⊢ Function.Injective ⇑g
Tactic:
exact this
Proof state after:
case intro.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this✝ :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
this : Set.Finite (⇑g ⁻¹' (⇑g '' Set.extremePoints ℝ (Hpolytope hH_)))
⊢ Function.Injective ⇑g
Theorem: Vpolytope_of_Hpolytope
Proof state before:
case intro.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this✝ :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
hgfPH : ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
hgExFin : Set.Finite (⇑g '' Set.extremePoints ℝ (Hpolytope hH_))
this : Set.Finite (⇑g ⁻¹' (⇑g '' Set.extremePoints ℝ (Hpolytope hH_)))
⊢ Function.Injective ⇑g
Tactic:
exact g.2
Proof state after:
no goals
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
⊢ ⇑g '' Set.extremePoints ℝ (Hpolytope hH_) ⊆ f '' PH
Tactic:
intro Sx hSx
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
Sx : Set E
hSx : Sx ∈ ⇑g '' Set.extremePoints ℝ (Hpolytope hH_)
⊢ Sx ∈ f '' PH
Theorem: Vpolytope_of_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
Sx : Set E
hSx : Sx ∈ ⇑g '' Set.extremePoints ℝ (Hpolytope hH_)
⊢ Sx ∈ f '' PH
Tactic:
rcases hSx with ⟨ x, hx, rfl ⟩
Proof state after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHcpt : IsCompact (Hpolytope hH_)
this :
  ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
f : Set (Halfspace E) → Set E := fun T => ⋂₀ ((fun x => frontier ↑x) '' T)
g : E ↪ Set E := { toFun := fun x => Set.singleton x, inj' := ⋯ }
Hfin : Finset (Halfspace E)
hHfin : ↑Hfin = H_
PHfin : Finset (Finset (Halfspace E)) := Finset.powerset Hfin
PH : Set (Set (Halfspace E)) := Finset.toSet '' ↑PHfin
hPH : Set.Finite PH
hfPH : Set.Finite (f '' PH)
x : E
hx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ g x ∈ f '' PH