Theorem: Closed_cutSpace (src/Cutspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ IsClosed (cutSpace H_)
Tactic:
apply isClosed_sInter
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ ∀ 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)
⊢ ∀ 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)
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)
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)
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)
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)
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)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ IsClosed {x | x ≤ Hi_.α}
Tactic:
exact isClosed_Iic
State after:
no goals