internlm/Lean-Github huggingface dataset:
Theorem: Vpolytope_of_Hpolytope
Proof 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
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_)
⊢ {x} ∈ f '' PH
Theorem: Vpolytope_of_Hpolytope
Proof 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]
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_)
⊢ ∃ x_1 ∈ PH, f x_1 = {x}
Theorem: Vpolytope_of_Hpolytope
Proof 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, ?_, ?_ ⟩
Proof 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}
Theorem: Vpolytope_of_Hpolytope
Proof 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]
Proof 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
Theorem: Vpolytope_of_Hpolytope
Proof 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 ⟩
Proof 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
Theorem: Vpolytope_of_Hpolytope
Proof 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 ⟩
Proof 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
Theorem: Vpolytope_of_Hpolytope
Proof 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]
Proof 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_
Theorem: Vpolytope_of_Hpolytope
Proof 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
Proof state after:
no goals
Theorem: Vpolytope_of_Hpolytope
Proof 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)]
Proof 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_)
Theorem: Vpolytope_of_Hpolytope
Proof 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
Proof state after:
no goals
Theorem: Hpolytope_of_Vpolytope_subsingleton
Proof state before:
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
cases' hStrivial.eq_empty_or_singleton with hSempty hSsingleton
Proof state after:
case inl
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSempty : S = ∅
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

case inr
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSsingleton : ∃ x, S = {x}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: Hpolytope_of_Vpolytope_subsingleton
Proof state before:
case inl
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSempty : S = ∅
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rw [Vpolytope, hSempty, convexHull_empty]
Proof state after:
case inl
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSempty : S = ∅
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Theorem: Hpolytope_of_Vpolytope_subsingleton
Proof state before:
case inl
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSempty : S = ∅
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
exact empty_Hpolytope
Proof state after:
no goals
Theorem: Hpolytope_of_Vpolytope_subsingleton
Proof state before:
case inr
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSsingleton : ∃ x, S = {x}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases hSsingleton with ⟨ x, hx ⟩
Proof state after:
case inr.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: Hpolytope_of_Vpolytope_subsingleton
Proof state before:
case inr.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases @origin_Hpolytope E _ _ _ _ with ⟨ H_, hH_Fin, hH_ ⟩
Proof state after:
case inr.intro.intro.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
H_ : Set (Halfspace E)
hH_Fin : Set.Finite H_
hH_ : Hpolytope hH_Fin = {0}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: Hpolytope_of_Vpolytope_subsingleton
Proof state before:
case inr.intro.intro.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
H_ : Set (Halfspace E)
hH_Fin : Set.Finite H_
hH_ : Hpolytope hH_Fin = {0}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
refine ⟨ Halfspace_translation x '' H_, hH_Fin.image (Halfspace_translation x), ?_ ⟩
Proof state after:
case inr.intro.intro.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
H_ : Set (Halfspace E)
hH_Fin : Set.Finite H_
hH_ : Hpolytope hH_Fin = {0}
⊢ Hpolytope ⋯ = Vpolytope hS
Theorem: Hpolytope_of_Vpolytope_subsingleton
Proof state before:
case inr.intro.intro.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
H_ : Set (Halfspace E)
hH_Fin : Set.Finite H_
hH_ : Hpolytope hH_Fin = {0}
⊢ Hpolytope ⋯ = Vpolytope hS
Tactic:
rw [Vpolytope, hx, convexHull_singleton, Hpolytope_translation hH_Fin, hH_, Set.singleton_add_singleton, zero_add]
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_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases DualOfVpolytope_compactHpolytope hS hV0 with ⟨ H_, hH_, hH_eq, hH_cpt ⟩
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: Hpolytope_of_Vpolytope_0interior
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases Vpolytope_of_Hpolytope hH_ hH_cpt with ⟨ S', hS', hS'eq ⟩
Proof state after:
case intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
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'
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have : 0 ∈ interior (Vpolytope hS') := by
  rw [←hS'eq, hH_eq, compact_polarDual_iff (Closed_Vpolytope hS)]
  exact Compact_Vpolytope hS
Proof state after:
case intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hV0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hH_eq : Hpolytope hH_ = polarDual (Vpolytope hS)
hH_cpt : IsCompact (Hpolytope hH_)
S' : Set E
hS' : Set.Finite S'
hS'eq : Hpolytope hH_ = Vpolytope hS'
this : 0 ∈ interior (Vpolytope hS')
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS