Theorem: Vpolytope_of_Hpolytope (src/MainTheorem.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ ∀ {H_ : Set (Halfspace E)} (hH_ : Set.Finite H_),
    IsCompact (Hpolytope hH_) → ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Tactic:
intro H_ hH_ hHcpt
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_)
⊢ ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS

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_))
⊢ ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Tactic:
have : closure (convexHull ℝ ((Hpolytope hH_).extremePoints ℝ)) = Hpolytope hH_ :=
  closure_convexHull_extremePoints hHcpt (Convex_Hpolytope hH_)
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_
⊢ ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS

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_
⊢ ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Tactic:
rw [← this, IsClosed.closure_eq]
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_
⊢ ∃ S, ∃ (hS : Set.Finite S), (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hS

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_)))

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_
⊢ ∃ S, ∃ (hS : Set.Finite S), (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hS

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:
use (Hpolytope hH_).extremePoints ℝ
State after:
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_
⊢ ∃ (hS : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))),
    (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hS

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_)))

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_
⊢ ∃ (hS : Set.Finite (Set.extremePoints ℝ (Hpolytope hH_))),
    (convexHull ℝ) (Set.extremePoints ℝ (Hpolytope hH_)) = Vpolytope hS

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:
use hExHFinite
State after:
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_)))

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
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_)))

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
State after:
no goals

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_
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_))

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 ⟩
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_))

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 ⟩
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_))

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
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_))

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
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_))

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 _
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_))

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
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_))

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
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_))

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
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_))

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
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

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
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

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
State after:
no goals

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
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

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 ⟩
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

State before:
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
Tactic:
change {x} ∈ f '' PH
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_)
⊢ {x} ∈ f '' PH

State before:
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_)
⊢ {x} ∈ f '' PH
Tactic:
rw [PH.mem_image]
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_)
⊢ ∃ x_1 ∈ PH, f x_1 = {x}

State before:
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_)
⊢ ∃ x_1 ∈ PH, f x_1 = {x}
Tactic:
refine ⟨ Hpolytope.I H_ x, ?_, ?_ ⟩
State after:
case intro.intro.refine_1
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_)
⊢ Hpolytope.I H_ x ∈ PH

case intro.intro.refine_2
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_)
⊢ f (Hpolytope.I H_ x) = {x}

State before:
case intro.intro.refine_1
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_)
⊢ Hpolytope.I H_ x ∈ PH
Tactic:
rw [Set.mem_image]
State after:
case intro.intro.refine_1
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_)
⊢ ∃ x_1 ∈ ↑PHfin, ↑x_1 = Hpolytope.I H_ x

State before:
case intro.intro.refine_1
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_)
⊢ ∃ x_1 ∈ ↑PHfin, ↑x_1 = Hpolytope.I H_ x
Tactic:
rcases (hH_.subset (Hpolytope.I_sub x)).exists_finset_coe  with ⟨ Ifin, hIfin ⟩
State after:
case intro.intro.refine_1.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_)
Ifin : Finset (Halfspace E)
hIfin : ↑Ifin = Hpolytope.I H_ x
⊢ ∃ x_1 ∈ ↑PHfin, ↑x_1 = Hpolytope.I H_ x

State before:
case intro.intro.refine_1.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_)
Ifin : Finset (Halfspace E)
hIfin : ↑Ifin = Hpolytope.I H_ x
⊢ ∃ x_1 ∈ ↑PHfin, ↑x_1 = Hpolytope.I H_ x
Tactic:
refine ⟨ Ifin, ?_, hIfin ⟩
State after:
case intro.intro.refine_1.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_)
Ifin : Finset (Halfspace E)
hIfin : ↑Ifin = Hpolytope.I H_ x
⊢ Ifin ∈ ↑PHfin

State before:
case intro.intro.refine_1.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_)
Ifin : Finset (Halfspace E)
hIfin : ↑Ifin = Hpolytope.I H_ x
⊢ Ifin ∈ ↑PHfin
Tactic:
rw [Finset.mem_coe, Finset.mem_powerset, ← Finset.coe_subset, hHfin, hIfin]
State after:
case intro.intro.refine_1.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_)
Ifin : Finset (Halfspace E)
hIfin : ↑Ifin = Hpolytope.I H_ x
⊢ Hpolytope.I H_ x ⊆ H_

State before:
case intro.intro.refine_1.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_)
Ifin : Finset (Halfspace E)
hIfin : ↑Ifin = Hpolytope.I H_ x
⊢ Hpolytope.I H_ x ⊆ H_
Tactic:
exact Hpolytope.I_sub x
State after:
no goals

State before:
case intro.intro.refine_2
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_)
⊢ f (Hpolytope.I H_ x) = {x}
Tactic:
rw [← ExtremePointsofHpolytope hH_ x (extremePoints_subset hx)]
State after:
case intro.intro.refine_2
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_)
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_)

State before:
case intro.intro.refine_2
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_)
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
exact hx
State after:
no goals