α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u} ≤
    TopologicalSpace.generateFrom (preimage (restrict s) '' {m | ∃ s_1 x u x, m = CompactOpen.gen s_1 u})
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ compactOpen ≤ TopologicalSpace.induced (restrict s) compactOpen
simp only [induced_generateFrom_eq, ContinuousMap.compactOpen]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ preimage (restrict s) '' {m | ∃ s_1 x u x, m = CompactOpen.gen s_1 u} ⊆ {m | ∃ s x u x, m = CompactOpen.gen s u}
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u} ≤
    TopologicalSpace.generateFrom (preimage (restrict s) '' {m | ∃ s_1 x u x, m = CompactOpen.gen s_1 u})
apply TopologicalSpace.generateFrom_anti
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen c u ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
case h
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ preimage (restrict s) '' {m | ∃ s_1 x u x, m = CompactOpen.gen s_1 u} ⊆ {m | ∃ s x u x, m = CompactOpen.gen s u}
rintro b ⟨a, ⟨c, hc, u, hu, rfl⟩, rfl⟩
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen c u = CompactOpen.gen (Subtype.val '' c) u
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen c u ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
refine' ⟨(↑) '' c, hc.image continuous_subtype_val, u, hu, _⟩
case h.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ f ∈ restrict s ⁻¹' CompactOpen.gen c u ↔ f ∈ CompactOpen.gen (Subtype.val '' c) u
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen c u = CompactOpen.gen (Subtype.val '' c) u
ext f
case h.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ (fun a => (↑f ∘ Subtype.val) a) '' c ⊆ u ↔ (fun a => ↑f a) '' (Subtype.val '' c) ⊆ u
case h.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ f ∈ restrict s ⁻¹' CompactOpen.gen c u ↔ f ∈ CompactOpen.gen (Subtype.val '' c) u
simp only [CompactOpen.gen, mem_setOf_eq, mem_preimage, ContinuousMap.coe_restrict]
no goals
case h.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.16761
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ (fun a => (↑f ∘ Subtype.val) a) '' c ⊆ u ↔ (fun a => ↑f a) '' (Subtype.val '' c) ⊆ u
rw [image_comp f ((↑) : s → α)]