[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.666
W : Type ?u.669
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
e : X ≃ₜ Y
⊢ IsProperMap ↑e
[PROOFSTEP]
rw [isProperMap_iff_clusterPt]
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.666
W : Type ?u.669
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
e : X ≃ₜ Y
⊢ Continuous ↑e ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ ↑e → ∃ x, ↑e x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
refine ⟨e.continuous, fun ℱ y ↦ ?_⟩
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.666
W : Type ?u.669
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
e : X ≃ₜ Y
ℱ : Filter X
y : Y
⊢ MapClusterPt y ℱ ↑e → ∃ x, ↑e x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, e.comap_nhds_eq, ← e.coe_toEquiv, ←
  e.eq_symm_apply, exists_eq_left]
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.666
W : Type ?u.669
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
e : X ≃ₜ Y
ℱ : Filter X
y : Y
⊢ NeBot (𝓝 (↑(Homeomorph.symm e) y) ⊓ ℱ) → NeBot (𝓝 (↑e.symm y) ⊓ ℱ)
[PROOFSTEP]
exact id
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.2964
W : Type ?u.2967
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
⊢ IsClosedMap f
[PROOFSTEP]
rw [isClosedMap_iff_clusterPt]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.2964
W : Type ?u.2967
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
[PROOFSTEP]
exact fun s y ↦ h.clusterPt_of_mapClusterPt (ℱ := 𝓟 s) (y := y)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rw [isProperMap_iff_clusterPt]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ (Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔
    Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine and_congr_right (fun _ ↦ ?_)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
⊢ (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
⊢ (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) →
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
intro H
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
⊢ (∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x) →
    ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
intro H
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
⊢ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
intro 𝒰 y (hY : (Ultrafilter.map f 𝒰 : Filter Y) ≤ _)
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
simp_rw [← Ultrafilter.clusterPt_iff] at hY ⊢
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : ClusterPt y ↑(Ultrafilter.map f 𝒰)
⊢ ∃ x, f x = y ∧ ClusterPt x ↑𝒰
[PROOFSTEP]
exact H hY
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, ← exists_ultrafilter_iff, forall_exists_index]
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄ (x : Ultrafilter X), ↑x ≤ comap f (𝓝 y) ⊓ ℱ → ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ
[PROOFSTEP]
intro ℱ y 𝒰 hy
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : ↑𝒰 ≤ comap f (𝓝 y) ⊓ ℱ
⊢ ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ
[PROOFSTEP]
rcases H (tendsto_iff_comap.mpr <| hy.trans inf_le_left) with ⟨x, hxy, hx⟩
[GOAL]
case mpr.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : ↑𝒰 ≤ comap f (𝓝 y) ⊓ ℱ
x : X
hxy : f x = y
hx : ↑𝒰 ≤ 𝓝 x
⊢ ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ
[PROOFSTEP]
exact ⟨x, hxy, 𝒰, le_inf hx (hy.trans inf_le_right)⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsProperMap f
hg : IsProperMap g
⊢ IsProperMap (Prod.map f g)
[PROOFSTEP]
simp_rw [isProperMap_iff_ultrafilter] at hf hg ⊢
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous (Prod.map f g) ∧
    ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄, Tendsto (Prod.map f g) (↑𝒰) (𝓝 y) → ∃ x, Prod.map f g x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
constructor
  -- Continuity is clear.
[GOAL]
case left
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous (Prod.map f g)
[PROOFSTEP]
exact
  hf.1.prod_map
    hg.1
      -- Let `𝒰 : Ultrafilter (X × Z)`, and assume that `f × g` tends to some `(y, w) : Y × W`
        -- along `𝒰`.
[GOAL]
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄, Tendsto (Prod.map f g) (↑𝒰) (𝓝 y) → ∃ x, Prod.map f g x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
intro 𝒰 ⟨y, w⟩ hyw
[GOAL]
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (Prod.map f g) (↑𝒰) (𝓝 (y, w))
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
simp_rw [nhds_prod_eq, tendsto_prod_iff'] at hyw 
[GOAL]
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases hf.2 (show Tendsto f (Ultrafilter.map fst 𝒰) (𝓝 y) by simpa using hyw.1) with ⟨x, hxy, hx⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
⊢ Tendsto f (↑(Ultrafilter.map fst 𝒰)) (𝓝 y)
[PROOFSTEP]
simpa using hyw.1
[GOAL]
case right.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases hg.2 (show Tendsto g (Ultrafilter.map snd 𝒰) (𝓝 w) by simpa using hyw.2) with
  ⟨z, hzw, hz⟩
    -- By the properties of the product topology, that means that `𝒰` tends to `(x, z)`,
      -- which completes the proof since `(f × g)(x, z) = (y, w)`.
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
⊢ Tendsto g (↑(Ultrafilter.map snd 𝒰)) (𝓝 w)
[PROOFSTEP]
simpa using hyw.2
[GOAL]
case right.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine ⟨⟨x, z⟩, Prod.ext hxy hzw, ?_⟩
[GOAL]
case right.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ ↑𝒰 ≤ 𝓝 (x, z)
[PROOFSTEP]
rw [nhds_prod_eq, le_prod]
[GOAL]
case right.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ Tendsto fst (↑𝒰) (𝓝 x) ∧ Tendsto snd (↑𝒰) (𝓝 z)
[PROOFSTEP]
exact ⟨hx, hz⟩
[GOAL]
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h : ∀ (i : ι), IsProperMap (f i)
⊢ IsProperMap fun x i => f i (x i)
[PROOFSTEP]
simp_rw [isProperMap_iff_ultrafilter] at h ⊢
[GOAL]
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ (Continuous fun x i => f i (x i)) ∧
    ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
      Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
constructor
  -- Continuity is clear.
[GOAL]
case left
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous fun x i => f i (x i)
[PROOFSTEP]
exact
  continuous_pi fun i ↦
    (h i).1.comp
      (continuous_apply i)
        -- Let `𝒰 : Ultrafilter (Π i, X i)`, and assume that `Π i, f i` tends to some `y : Π i, Y i`
          -- along `𝒰`.
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
intro 𝒰 y hy
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have : ∀ i, Tendsto (f i) (Ultrafilter.map (eval i) 𝒰) (𝓝 (y i)) := by simpa [tendsto_pi_nhds] using hy
[GOAL]
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
⊢ ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
[PROOFSTEP]
simpa [tendsto_pi_nhds] using hy
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
choose x hxy hx using fun i ↦
  (h i).2
    (this i)
      -- By the properties of the product topology, that means that `𝒰` tends to `x`,
        -- which completes the proof since `(Π i, f i) x = y`.
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine ⟨x, funext hxy, ?_⟩
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rwa [nhds_pi, le_pi]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)
[PROOFSTEP]
rw [isCompact_iff_ultrafilter_le_nhds]
  -- Let `𝒰 ≤ 𝓟 (f ⁻¹' K)` an ultrafilter.
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ ∀ (f_1 : Ultrafilter X), ↑f_1 ≤ 𝓟 (f ⁻¹' K) → ∃ a, a ∈ f ⁻¹' K ∧ ↑f_1 ≤ 𝓝 a
[PROOFSTEP]
intro 𝒰 h𝒰
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
⊢ ∃ a, a ∈ f ⁻¹' K ∧ ↑𝒰 ≤ 𝓝 a
[PROOFSTEP]
rw [← comap_principal, ← map_le_iff_le_comap, ← Ultrafilter.coe_map] at h𝒰 
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
⊢ ∃ a, a ∈ f ⁻¹' K ∧ ↑𝒰 ≤ 𝓝 a
[PROOFSTEP]
rcases hK.ultrafilter_le_nhds _ h𝒰 with
  ⟨y, hyK, hy⟩
    -- Then, by properness of `f`, that means that `𝒰` tends to some `x ∈ f ⁻¹' {y} ⊆ f ⁻¹' K`,
      -- which completes the proof.
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
y : Y
hyK : y ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y
⊢ ∃ a, a ∈ f ⁻¹' K ∧ ↑𝒰 ≤ 𝓝 a
[PROOFSTEP]
rcases h.ultrafilter_le_nhds_of_tendsto hy with ⟨x, rfl, hx⟩
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
x : X
hx : ↑𝒰 ≤ 𝓝 x
hyK : f x ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 (f x)
⊢ ∃ a, a ∈ f ⁻¹' K ∧ ↑𝒰 ≤ 𝓝 a
[PROOFSTEP]
exact ⟨x, hyK, hx⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
[PROOFSTEP]
intro H
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ (Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
[PROOFSTEP]
exact ⟨H.continuous, H.isClosedMap, fun y ↦ H.isCompact_preimage isCompact_singleton⟩
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_clusterPt]
  -- Let `ℱ : Filter X` and `y` some cluster point of `map f ℱ`.
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
refine
  ⟨H.1, fun ℱ y hy ↦ ?_⟩
    -- That means that the singleton `pure y` meets the "closure" of `map f ℱ`, by which we mean
      -- `Filter.lift' (map f ℱ) closure`. But `f` is closed, so
      -- `closure (map f ℱ) = map f (closure ℱ)` (see `IsClosedMap.lift'_closure_map_eq`).
      -- Thus `map f (closure ℱ ⊓ 𝓟 (f ⁻¹' {y})) = map f (closure ℱ) ⊓ 𝓟 {y} ≠ ⊥`, hence
      -- `closure ℱ ⊓ 𝓟 (f ⁻¹' {y}) ≠ ⊥`.
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : MapClusterPt y ℱ f
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
rw [H.2.1.mapClusterPt_iff_lift'_closure H.1] at hy 
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : NeBot (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
rcases H.2.2 y (f := Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' { y })) inf_le_right with ⟨x, hxy, hx⟩
[GOAL]
case mpr.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : NeBot (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
refine
  ⟨x, hxy, ?_⟩
    -- In particular `x` is a cluster point of `closure ℱ`. Since cluster points of `closure ℱ`
      -- are exactly cluster points of `ℱ` (see `clusterPt_lift'_closure_iff`), this completes
      -- the proof.
[GOAL]
case mpr.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : NeBot (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x ℱ
[PROOFSTEP]
rw [← clusterPt_lift'_closure_iff]
[GOAL]
case mpr.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : NeBot (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x (Filter.lift' ℱ closure)
[PROOFSTEP]
exact hx.mono inf_le_left
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.37764
W : Type ?u.37767
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace W
f : X → Y
inst✝ : T1Space Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite
[PROOFSTEP]
simp_rw [isProperMap_iff_isClosedMap_and_compact_fibers, Tendsto, le_cofinite_iff_compl_singleton_mem, mem_map,
  preimage_compl]
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.37764
W : Type ?u.37767
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace W
f : X → Y
inst✝ : T1Space Y
⊢ (Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
[PROOFSTEP]
refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦ ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.37764
W : Type ?u.37767
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace W
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
⊢ IsCompact (f ⁻¹' {y})
[PROOFSTEP]
rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩
[GOAL]
case intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.37764
W : Type ?u.37767
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace W
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
K : Set X
hK : IsCompact K
hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ
⊢ IsCompact (f ⁻¹' {y})
[PROOFSTEP]
exact isCompact_of_isClosed_subset hK (isClosed_singleton.preimage f_cont) (compl_le_compl_iff_le.mp hKy)
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ IsProperMap f → Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
[PROOFSTEP]
intro H
[GOAL]
case mpr
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
[PROOFSTEP]
exact ⟨H.continuous, fun K hK ↦ H.isCompact_preimage hK⟩
[GOAL]
case mpr
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_ultrafilter]
  -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.
[GOAL]
case mpr
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine
  ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
    -- Pick `K` some compact neighborhood of `y`, which exists by local compactness.
[GOAL]
case mpr
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases exists_compact_mem_nhds y with
  ⟨K, hK, hKy⟩
    -- Then `map f 𝒰 ≤ 𝓝 y ≤ 𝓟 K`, hence `𝒰 ≤ 𝓟 (f ⁻¹' K)`
[GOAL]
case mpr.intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
K : Set Y
hK : IsCompact K
hKy : K ∈ 𝓝 y
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have : 𝒰 ≤ 𝓟 (f ⁻¹' K) := by
  simpa only [← comap_principal, ← tendsto_iff_comap] using
    hy.mono_right
      (le_principal_iff.mpr hKy)
        -- By compactness of `f ⁻¹' K`, `𝒰` converges to some `x ∈ f ⁻¹' K`.
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
K : Set Y
hK : IsCompact K
hKy : K ∈ 𝓝 y
⊢ ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
[PROOFSTEP]
simpa only [← comap_principal, ← tendsto_iff_comap] using
  hy.mono_right
    (le_principal_iff.mpr hKy)
      -- By compactness of `f ⁻¹' K`, `𝒰` converges to some `x ∈ f ⁻¹' K`.
[GOAL]
case mpr.intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
K : Set Y
hK : IsCompact K
hKy : K ∈ 𝓝 y
this : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases(H.2 hK).ultrafilter_le_nhds _ this with
  ⟨x, -, hx⟩
    -- Finally, `f` tends to `f x` along `𝒰` by continuity, thus `f x = y`.
[GOAL]
case mpr.intro.intro.intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
K : Set Y
hK : IsCompact K
hKy : K ∈ 𝓝 y
this : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
x : X
hx : ↑𝒰 ≤ 𝓝 x
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine ⟨x, tendsto_nhds_unique ((H.1.tendsto _).comp hx) hy, hx⟩
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.49990
W : Type ?u.49993
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)
[PROOFSTEP]
simp_rw [isProperMap_iff_isCompact_preimage, hasBasis_cocompact.tendsto_right_iff, ← mem_preimage, eventually_mem_set,
  preimage_compl]
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.49990
W : Type ?u.49993
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
[PROOFSTEP]
refine and_congr_right fun f_cont ↦ ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.49990
W : Type ?u.49993
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)
[PROOFSTEP]
rcases mem_cocompact.mp (H K hK) with ⟨K', hK', hK'y⟩
[GOAL]
case intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.49990
W : Type ?u.49993
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ
⊢ IsCompact (f ⁻¹' K)
[PROOFSTEP]
exact isCompact_of_isClosed_subset hK' (hK.isClosed.preimage f_cont) (compl_le_compl_iff_le.mp hK'y)
[GOAL]
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
constructor
[GOAL]
case mp
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
intro H
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ∧ IsClosedMap (Prod.map f id) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
exact ⟨H.continuous, H.universally_closed _⟩
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_ultrafilter]
  -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine
  ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
    -- In `X × Filter X`, consider the closed set `F := closure {(x, ℱ) | ℱ = pure x}`
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
let F : Set (X × Filter X) :=
  closure
    {xℱ | xℱ.2 = pure xℱ.1}
      -- Since `f × id` is closed, the set `(f × id) '' F` is also closed.
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have := H.2 F isClosed_closure
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have : (y, ↑𝒰) ∈ Prod.map f id '' F :=
  -- Note that, by the properties of the topology on `Filter X`, the function `pure : X → Filter X`
    -- tends to the point `𝒰` of `Filter X` along the filter `𝒰` on `X`. Since `f` tends to `y` along
    -- `𝒰`, we get that the function `(f, pure) : X → (Y, Filter X)` tends to `(y, 𝒰)` along
    -- `𝒰`. Furthermore, each `(f, pure)(x) = (f × id)(x, pure x)` is clearly an element of
    -- the closed set `(f × id) '' F`, thus the limit `(y, 𝒰)` also belongs to that set.this.mem_of_tendsto
    (hy.prod_mk_nhds (Filter.tendsto_pure_self (𝒰 : Filter X)))
    (eventually_of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
      -- The above shows that `(y, 𝒰) = (f x, 𝒰)`, for some `x : X` such that `(x, 𝒰) ∈ F`.
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this✝ : IsClosed (Prod.map f id '' F)
this : (y, ↑𝒰) ∈ Prod.map f id '' F
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases this with
  ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
    -- We already know that `f x = y`, so to finish the proof we just have to check that `𝒰` tends
      -- to `x`. So, for `U ∈ 𝓝 x` arbitrary, let's show that `U ∈ 𝒰`. Since `𝒰` is a ultrafilter,
      -- it is enough to show that `Uᶜ` is not in `𝒰`.
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (𝓝 (f x))
hx : (x, 𝒰.1) ∈ F
⊢ ∃ x_1, f x_1 = f x ∧ ↑𝒰 ≤ 𝓝 x_1
[PROOFSTEP]
refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_not_mem_iff.mp fun hUc ↦ ?_⟩
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (𝓝 (f x))
hx : (x, 𝒰.1) ∈ F
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ 𝒰
⊢ False
[PROOFSTEP]
rw [mem_closure_iff_nhds] at hx 
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (𝓝 (f x))
hx : ∀ (t : Set (X × Filter X)), t ∈ 𝓝 (x, 𝒰.1) → Set.Nonempty (t ∩ {xℱ | xℱ.snd = pure xℱ.fst})
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ 𝒰
⊢ False
[PROOFSTEP]
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU (isOpen_setOf_mem.mem_nhds hUc)) with
  ⟨⟨z, 𝒢⟩, ⟨⟨hz : z ∈ U, hz' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure z⟩⟩
[GOAL]
case mpr.intro.mk.intro.refl.intro.mk.intro.intro
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (𝓝 (f x))
hx : ∀ (t : Set (X × Filter X)), t ∈ 𝓝 (x, 𝒰.1) → Set.Nonempty (t ∩ {xℱ | xℱ.snd = pure xℱ.fst})
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ 𝒰
z : X
hz : z ∈ U
hz' : Uᶜ ∈ pure z
⊢ False
[PROOFSTEP]
exact hz' hz
[GOAL]
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
constructor
[GOAL]
case mp
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
intro H
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ∧ IsClosedMap (Prod.map f id) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
exact ⟨H.continuous, H.universally_closed _⟩
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_ultrafilter]
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
let F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have := H.2 F isClosed_closure
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have : (y, 𝒰) ∈ Prod.map f id '' F :=
  this.mem_of_tendsto (hy.prod_mk_nhds (Ultrafilter.tendsto_pure_self 𝒰))
    (eventually_of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this✝ : IsClosed (Prod.map f id '' F)
this : (y, 𝒰) ∈ Prod.map f id '' F
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : (x, snd✝) ∈ F
hy : Tendsto f (↑(id snd✝)) (𝓝 (f x))
⊢ ∃ x_1, f x_1 = f x ∧ ↑(id snd✝) ≤ 𝓝 x_1
[PROOFSTEP]
refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_not_mem_iff.mp fun hUc ↦ ?_⟩
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : (x, snd✝) ∈ F
hy : Tendsto f (↑(id snd✝)) (𝓝 (f x))
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ id snd✝
⊢ False
[PROOFSTEP]
rw [mem_closure_iff_nhds] at hx 
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ (t : Set (X × Ultrafilter X)), t ∈ 𝓝 (x, snd✝) → Set.Nonempty (t ∩ {xℱ | xℱ.snd = pure xℱ.fst})
hy : Tendsto f (↑(id snd✝)) (𝓝 (f x))
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ id snd✝
⊢ False
[PROOFSTEP]
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU ((ultrafilter_isOpen_basic _).mem_nhds hUc)) with
  ⟨⟨y, 𝒢⟩, ⟨⟨hy : y ∈ U, hy' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure y⟩⟩
[GOAL]
case mpr.intro.mk.intro.refl.intro.mk.intro.intro
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ (t : Set (X × Ultrafilter X)), t ∈ 𝓝 (x, snd✝) → Set.Nonempty (t ∩ {xℱ | xℱ.snd = pure xℱ.fst})
hy✝ : Tendsto f (↑(id snd✝)) (𝓝 (f x))
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ id snd✝
y : X
hy : y ∈ U
hy' : Uᶜ ∈ pure y
⊢ False
[PROOFSTEP]
exact hy' hy
[GOAL]
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
[PROOFSTEP]
constructor
[GOAL]
case mp
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
[PROOFSTEP]
intro H
[GOAL]
case mpr
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
[PROOFSTEP]
exact ⟨H.continuous, fun Z ↦ H.universally_closed _⟩
[GOAL]
case mpr
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_isClosedMap_ultrafilter]
[GOAL]
case mpr
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
exact ⟨H.1, H.2 _⟩
