case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ compactOpen ≤ ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ (⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen) ≤ compactOpen
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ compactOpen = ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen
refine' le_antisymm _ _
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ TopologicalSpace.generateFrom
      (⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}) ≤
    TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u}
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ (⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen) ≤ compactOpen
simp only [← generateFrom_iUnion, induced_generateFrom_eq, ContinuousMap.compactOpen]
case refine'_2.h
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ {m | ∃ s x u x, m = CompactOpen.gen s u} ⊆
    ⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ TopologicalSpace.generateFrom
      (⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}) ≤
    TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u}
apply TopologicalSpace.generateFrom_anti
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ CompactOpen.gen s u ∈
    ⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
case refine'_2.h
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ {m | ∃ s x u x, m = CompactOpen.gen s u} ⊆
    ⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
rintro _ ⟨s, hs, u, hu, rfl⟩
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ ∃ i j, CompactOpen.gen s u ∈ preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ CompactOpen.gen s u ∈
    ⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
rw [mem_iUnion₂]
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen univ u = CompactOpen.gen s u
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ ∃ i j, CompactOpen.gen s u ∈ preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
refine' ⟨s, hs, _, ⟨univ, isCompact_iff_isCompact_univ.mp hs, u, hu, rfl⟩, _⟩
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ f ∈ restrict s ⁻¹' CompactOpen.gen univ u ↔ f ∈ CompactOpen.gen s u
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen univ u = CompactOpen.gen s u
ext f
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ (fun a => (↑f ∘ Subtype.val) a) '' univ ⊆ u ↔ (fun a => ↑f a) '' s ⊆ u
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ f ∈ restrict s ⁻¹' CompactOpen.gen univ u ↔ f ∈ CompactOpen.gen s u
simp only [CompactOpen.gen, mem_setOf_eq, mem_preimage, ContinuousMap.coe_restrict]
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ ↑f '' (Subtype.val '' univ) ⊆ u ↔ (fun a => ↑f a) '' s ⊆ u
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ (fun a => (↑f ∘ Subtype.val) a) '' univ ⊆ u ↔ (fun a => ↑f a) '' s ⊆ u
rw [image_comp f ((↑) : s → α)]
no goals
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ ↑f '' (Subtype.val '' univ) ⊆ u ↔ (fun a => ↑f a) '' s ⊆ u
simp
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ∀ (i : Set α), IsCompact i → compactOpen ≤ TopologicalSpace.induced (restrict i) compactOpen
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ compactOpen ≤ ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen
refine' le_iInf₂ _
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19379
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ∀ (i : Set α), IsCompact i → compactOpen ≤ TopologicalSpace.induced (restrict i) compactOpen
exact fun s _ => compactOpen_le_induced s