Theorem: IsClosed_𝓜 (RMT4/Spaces.lean)

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (𝓜 U)
Tactic:
suffices h : IsClosed {f : 𝓒 U | MapsTo f U (closedBall 0 1)} by
  exact (isClosed_𝓗 hU).inter h
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed {f | MapsTo f U (closedBall 0 1)}

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed {f | MapsTo f U (closedBall 0 1)}
Tactic:
simp_rw [MapsTo, setOf_forall]
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (⋂ i ∈ U, {x | x i ∈ closedBall 0 1})

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (⋂ i ∈ U, {x | x i ∈ closedBall 0 1})
Tactic:
refine isClosed_biInter (λ z hz => isClosed_ball.preimage ?_)
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
z : ℂ
hz : z ∈ U
⊢ Continuous fun x => x z

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
z : ℂ
hz : z ∈ U
⊢ Continuous fun x => x z
Tactic:
exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
  (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous)
State after:
no goals

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
h : IsClosed {f | MapsTo f U (closedBall 0 1)}
⊢ IsClosed (𝓜 U)
Tactic:
exact (isClosed_𝓗 hU).inter h
State after:
no goals