α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u} =
    TopologicalSpace.mkOfNhds fun f => FilterBasis.filter (compactConvergenceFilterBasis f)
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ compactOpen = compactConvergenceTopology
rw [compactConvergenceTopology, ContinuousMap.compactOpen]
case refine'_1
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u} ≤
    TopologicalSpace.mkOfNhds fun f => FilterBasis.filter (compactConvergenceFilterBasis f)

case refine'_2
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ (TopologicalSpace.mkOfNhds fun f => FilterBasis.filter (compactConvergenceFilterBasis f)) ≤
    TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u}
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u} =
    TopologicalSpace.mkOfNhds fun f => FilterBasis.filter (compactConvergenceFilterBasis f)
refine' le_antisymm _ _
case refine'_1
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
case refine'_1
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u} ≤
    TopologicalSpace.mkOfNhds fun f => FilterBasis.filter (compactConvergenceFilterBasis f)
refine' fun X hX => isOpen_iff_forall_mem_open.mpr fun f hf => _
case refine'_1
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
hXf : X ∈ FilterBasis.filter (compactConvergenceFilterBasis f)
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
case refine'_1
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
have hXf : X ∈ (compactConvergenceFilterBasis f).filter := by
  rw [← nhds_compactConvergence]
  exact @IsOpen.mem_nhds C(α, β) compactConvergenceTopology _ _ hX hf
case refine'_1.intro.intro.intro.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
hXf : (fun KV => compactConvNhd KV.fst KV.snd f) (K, V) ⊆ X
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
case refine'_1
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
hXf : X ∈ FilterBasis.filter (compactConvergenceFilterBasis f)
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
obtain ⟨-, ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩, hXf⟩ := hXf
case refine'_1.intro.intro.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
hXf : (fun KV => compactConvNhd KV.fst KV.snd f) (K, V) ⊆ X
ι : Type u₁
hι : Fintype ι
C : ι → Set α
hC : ∀ (i : ι), IsCompact (C i)
U : ι → Set β
hU : ∀ (i : ι), IsOpen (U i)
h₁ : f ∈ ⋂ (i : ι), CompactOpen.gen (C i) (U i)
h₂ : (⋂ (i : ι), CompactOpen.gen (C i) (U i)) ⊆ compactConvNhd (K, V).fst (K, V).snd f
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
case refine'_1.intro.intro.intro.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
hXf : (fun KV => compactConvNhd KV.fst KV.snd f) (K, V) ⊆ X
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
obtain ⟨ι, hι, C, hC, U, hU, h₁, h₂⟩ := iInter_compactOpen_gen_subset_compactConvNhd f hK hV
case refine'_1.intro.intro.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
hXf : (fun KV => compactConvNhd KV.fst KV.snd f) (K, V) ⊆ X
ι : Type u₁
hι : Fintype ι
C : ι → Set α
hC : ∀ (i : ι), IsCompact (C i)
U : ι → Set β
hU : ∀ (i : ι), IsOpen (U i)
h₁ : f ∈ ⋂ (i : ι), CompactOpen.gen (C i) (U i)
h₂ : (⋂ (i : ι), CompactOpen.gen (C i) (U i)) ⊆ compactConvNhd (K, V).fst (K, V).snd f
this : Fintype ι
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
case refine'_1.intro.intro.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
hXf : (fun KV => compactConvNhd KV.fst KV.snd f) (K, V) ⊆ X
ι : Type u₁
hι : Fintype ι
C : ι → Set α
hC : ∀ (i : ι), IsCompact (C i)
U : ι → Set β
hU : ∀ (i : ι), IsOpen (U i)
h₁ : f ∈ ⋂ (i : ι), CompactOpen.gen (C i) (U i)
h₂ : (⋂ (i : ι), CompactOpen.gen (C i) (U i)) ⊆ compactConvNhd (K, V).fst (K, V).snd f
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
haveI := hι
no goals
case refine'_1.intro.intro.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
hXf : (fun KV => compactConvNhd KV.fst KV.snd f) (K, V) ⊆ X
ι : Type u₁
hι : Fintype ι
C : ι → Set α
hC : ∀ (i : ι), IsCompact (C i)
U : ι → Set β
hU : ∀ (i : ι), IsOpen (U i)
h₁ : f ∈ ⋂ (i : ι), CompactOpen.gen (C i) (U i)
h₂ : (⋂ (i : ι), CompactOpen.gen (C i) (U i)) ⊆ compactConvNhd (K, V).fst (K, V).snd f
this : Fintype ι
⊢ ∃ t, t ⊆ X ∧ IsOpen t ∧ f ∈ t
exact
  ⟨⋂ i, CompactOpen.gen (C i) (U i), h₂.trans hXf,
    isOpen_iInter fun i => ContinuousMap.isOpen_gen (hC i) (hU i), h₁⟩
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
⊢ X ∈ 𝓝 f
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
⊢ X ∈ FilterBasis.filter (compactConvergenceFilterBasis f)
rw [← nhds_compactConvergence]
no goals
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ : C(α, β)
X : Set C(α, β)
hX : IsOpen X
f : C(α, β)
hf : f ∈ X
⊢ X ∈ 𝓝 f
exact @IsOpen.mem_nhds C(α, β) compactConvergenceTopology _ _ hX hf
case refine'_2
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ ∀ (a : Set C(α, β)) (x : Set α), IsCompact x → ∀ (x_1 : Set β), IsOpen x_1 → a = CompactOpen.gen x x_1 → IsOpen a
case refine'_2
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ (TopologicalSpace.mkOfNhds fun f => FilterBasis.filter (compactConvergenceFilterBasis f)) ≤
    TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u}
simp only [TopologicalSpace.le_generateFrom_iff_subset_isOpen, and_imp, exists_prop,
  forall_exists_index, setOf_subset_setOf]
case refine'_2
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f✝ : C(α, β)
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen U
f : C(α, β)
hf : f ∈ CompactOpen.gen K U
⊢ CompactOpen.gen K U ∈ (fun f => FilterBasis.filter (compactConvergenceFilterBasis f)) f
case refine'_2
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ ∀ (a : Set C(α, β)) (x : Set α), IsCompact x → ∀ (x_1 : Set β), IsOpen x_1 → a = CompactOpen.gen x x_1 → IsOpen a
rintro - K hK U hU rfl f hf
case refine'_2.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f✝ : C(α, β)
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen U
f : C(α, β)
hf : f ∈ CompactOpen.gen K U
V : Set (β × β)
hV : V ∈ 𝓤 β
_hV' : IsOpen V
hVf : compactConvNhd K V f ⊆ CompactOpen.gen K U
⊢ CompactOpen.gen K U ∈ (fun f => FilterBasis.filter (compactConvergenceFilterBasis f)) f
case refine'_2
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f✝ : C(α, β)
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen U
f : C(α, β)
hf : f ∈ CompactOpen.gen K U
⊢ CompactOpen.gen K U ∈ (fun f => FilterBasis.filter (compactConvergenceFilterBasis f)) f
obtain ⟨V, hV, _hV', hVf⟩ := compactConvNhd_subset_compactOpen f hK hU hf
no goals
case refine'_2.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f✝ : C(α, β)
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen U
f : C(α, β)
hf : f ∈ CompactOpen.gen K U
V : Set (β × β)
hV : V ∈ 𝓤 β
_hV' : IsOpen V
hVf : compactConvNhd K V f ⊆ CompactOpen.gen K U
⊢ CompactOpen.gen K U ∈ (fun f => FilterBasis.filter (compactConvergenceFilterBasis f)) f
exact Filter.mem_of_superset (FilterBasis.mem_filter_of_mem _ ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩) hVf