Theorem: isCompact_𝓑 (RMT4/Montel.lean)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsCompact (𝓑 U Q)
Tactic:
have l1 (K) (hK : K ∈ compacts U) : EquicontinuousOn ((↑) : 𝓑 U Q → 𝓒 U) K :=
  (uniformlyBoundedOn_𝓑 hQ).equicontinuousOn hU (fun f => f.2.1) hK
State after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
⊢ IsCompact (𝓑 U Q)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
⊢ IsCompact (𝓑 U Q)
Tactic:
have l2 (K) (hK : K ∈ compacts U) (x) (hx : x ∈ K) : ∃ L, IsCompact L ∧ ∀ i : 𝓑 U Q, i.1 x ∈ L :=
  ⟨Q K, hQ K hK, fun f => f.2.2 K hK hx⟩
State after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsCompact (𝓑 U Q)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsCompact (𝓑 U Q)
Tactic:
rw [isCompact_iff_compactSpace]
State after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ CompactSpace ↑(𝓑 U Q)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ CompactSpace ↑(𝓑 U Q)
Tactic:
refine ArzelaAscoli.compactSpace_of_closedEmbedding (fun K hK => hK.2) ?_ l1 l2
State after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ ClosedEmbedding (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ ClosedEmbedding (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val)
Tactic:
refine ⟨⟨by tauto, fun f g => Subtype.ext⟩, ?_⟩
State after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsClosed (range (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val))

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsClosed (range (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val))
Tactic:
simpa [range, UniformOnFun.ofFun] using isClosed_𝓑 hU hQ
State after:
no goals

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ Inducing (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val)
Tactic:
tauto
State after:
no goals