[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Tendsto f cofinite (cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → Set.Finite (f ⁻¹' K)
[PROOFSTEP]
rw [hasBasis_cocompact.tendsto_right_iff]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → Set.Finite (f ⁻¹' K)
[PROOFSTEP]
refine' forall₂_congr (fun K _ ↦ _)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
K : Set Y
x✝ : IsCompact K
⊢ (∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ Set.Finite (f ⁻¹' K)
[PROOFSTEP]
simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
⊢ DiscreteTopology X
[PROOFSTEP]
refine' singletons_open_iff_discrete.mp (fun x ↦ _)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
⊢ IsOpen {x}
[PROOFSTEP]
obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
⊢ IsOpen {x}
[PROOFSTEP]
obtain ⟨U : Set Y, hU₁ : U ⊆ K, hU₂ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen U
hU₃ : f x ∈ U
⊢ IsOpen {x}
[PROOFSTEP]
have hU₄ : Set.Finite (f ⁻¹' U) := Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen U
hU₃ : f x ∈ U
hU₄ : Set.Finite (f ⁻¹' U)
⊢ IsOpen {x}
[PROOFSTEP]
exact isOpen_singleton_of_finite_mem_nhds _ ((hU₂.preimage hf').mem_nhds hU₃) hU₄
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ Tendsto f cofinite (cocompact Y)
[PROOFSTEP]
convert hf
[GOAL]
case h.e'_4
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cocompact X
[PROOFSTEP]
rw [cocompact_eq_cofinite X]
