Theorem: isClosed_𝓑 (RMT4/Spaces.lean)

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed (𝓑 U Q)
Tactic:
rw [𝓑, setOf_and]
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed ({a | a ∈ 𝓗 U} ∩ {a | ∀ K ∈ compacts U, MapsTo a K (Q K)})

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed ({a | a ∈ 𝓗 U} ∩ {a | ∀ K ∈ compacts U, MapsTo a K (Q K)})
Tactic:
apply (isClosed_𝓗 hU).inter
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed {a | ∀ K ∈ compacts U, MapsTo a K (Q K)}

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed {a | ∀ K ∈ compacts U, MapsTo a K (Q K)}
Tactic:
simp only [setOf_forall, MapsTo]
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed (⋂ i ∈ compacts U, ⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed (⋂ i ∈ compacts U, ⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})
Tactic:
apply isClosed_biInter
State after:
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ ∀ i ∈ compacts U, IsClosed (⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})

State before:
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ ∀ i ∈ compacts U, IsClosed (⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})
Tactic:
intro K hK
State after:
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ IsClosed (⋂ i ∈ K, {x | x i ∈ Q K})

State before:
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ IsClosed (⋂ i ∈ K, {x | x i ∈ Q K})
Tactic:
apply isClosed_biInter
State after:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ ∀ i ∈ K, IsClosed {x | x i ∈ Q K}

State before:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ ∀ i ∈ K, IsClosed {x | x i ∈ Q K}
Tactic:
intro z hz
State after:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ IsClosed {x | x z ∈ Q K}

State before:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ IsClosed {x | x z ∈ Q K}
Tactic:
apply (hQ K hK).isClosed.preimage
State after:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ Continuous fun x => x z

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