Theorem: Closed_Hpolytope (src/Polytope.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
⊢ IsClosed (Hpolytope hH_)
Tactic:
apply isClosed_sInter
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
⊢ ∀ t ∈ SetLike.coe '' H, IsClosed t

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
⊢ ∀ t ∈ SetLike.coe '' H, IsClosed t
Tactic:
rintro _ ⟨ Hi_, _, rfl ⟩
State after:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed ↑Hi_

State before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed ↑Hi_
Tactic:
rw [Hi_.h]
State after:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α})

State before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α})
Tactic:
apply IsClosed.preimage (Hi_.f.1.cont)
State after:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed {x | x ≤ Hi_.α}

State before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H : Set (Halfspace E)
hH_ : Set.Finite H
Hi_ : Halfspace E
left✝ : Hi_ ∈ H
⊢ IsClosed {x | x ≤ Hi_.α}
Tactic:
exact isClosed_Iic
State after:
no goals