case mp
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
⊢ lim ↑f = lim ↑g → (f, g) ∈ 𝓢 (CauchyFilter α)

case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
⊢ (f, g) ∈ 𝓢 (CauchyFilter α) → lim ↑f = lim ↑g
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
⊢ lim ↑f = lim ↑g ↔ (f, g) ∈ 𝓢 (CauchyFilter α)
constructor
case mp
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
⊢ (f, g) ∈ s
case mp
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
⊢ lim ↑f = lim ↑g → (f, g) ∈ 𝓢 (CauchyFilter α)
intro e s hs
case mp.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
⊢ (f, g) ∈ s
case mp
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
⊢ (f, g) ∈ s
rcases CauchyFilter.mem_uniformity'.1 hs with ⟨t, tu, ts⟩
case mp.intro.intro.a
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
⊢ t ∈ ↑f ×ˢ ↑g
case mp.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
⊢ (f, g) ∈ s
apply ts
case mp.intro.intro.a.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
⊢ t ∈ ↑f ×ˢ ↑g
case mp.intro.intro.a
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
⊢ t ∈ ↑f ×ˢ ↑g
rcases comp_mem_uniformity_sets tu with ⟨d, du, dt⟩
case mp.intro.intro.a.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
x : α × α
h : x ∈ {x | (x, lim ↑f) ∈ d} ×ˢ {y | (lim ↑g, y) ∈ d}
⊢ x ∈ t
case mp.intro.intro.a.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
⊢ t ∈ ↑f ×ˢ ↑g
refine'
  mem_prod_iff.2
    ⟨_, f.2.le_nhds_lim (mem_nhds_right (lim f.1) du), _,
      g.2.le_nhds_lim (mem_nhds_left (lim g.1) du), fun x h => _⟩
case mp.intro.intro.a.intro.intro.mk
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h : (a, b) ∈ {x | (x, lim ↑f) ∈ d} ×ˢ {y | (lim ↑g, y) ∈ d}
⊢ (a, b) ∈ t
case mp.intro.intro.a.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
x : α × α
h : x ∈ {x | (x, lim ↑f) ∈ d} ×ˢ {y | (lim ↑g, y) ∈ d}
⊢ x ∈ t
cases' x with a b
case mp.intro.intro.a.intro.intro.mk.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h₁ : (a, b).fst ∈ {x | (x, lim ↑f) ∈ d}
h₂ : (a, b).snd ∈ {y | (lim ↑g, y) ∈ d}
⊢ (a, b) ∈ t
case mp.intro.intro.a.intro.intro.mk
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h : (a, b) ∈ {x | (x, lim ↑f) ∈ d} ×ˢ {y | (lim ↑g, y) ∈ d}
⊢ (a, b) ∈ t
cases' h with h₁ h₂
case mp.intro.intro.a.intro.intro.mk.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h₁ : (a, b).fst ∈ {x | (x, lim ↑f) ∈ d}
h₂ : (a, b).snd ∈ {y | (lim ↑f, y) ∈ d}
⊢ (a, b) ∈ t
case mp.intro.intro.a.intro.intro.mk.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h₁ : (a, b).fst ∈ {x | (x, lim ↑f) ∈ d}
h₂ : (a, b).snd ∈ {y | (lim ↑g, y) ∈ d}
⊢ (a, b) ∈ t
rw [← e] at h₂
no goals
case mp.intro.intro.a.intro.intro.mk.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h₁ : (a, b).fst ∈ {x | (x, lim ↑f) ∈ d}
h₂ : (a, b).snd ∈ {y | (lim ↑f, y) ∈ d}
⊢ (a, b) ∈ t
exact dt ⟨_, h₁, h₂⟩
case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
⊢ lim ↑f = lim ↑g
case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
⊢ (f, g) ∈ 𝓢 (CauchyFilter α) → lim ↑f = lim ↑g
intro H
case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
⊢ (lim ↑f, lim ↑g) ∈ t
case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
⊢ lim ↑f = lim ↑g
refine' separated_def.1 (by infer_instance) _ _ fun t tu => _
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
⊢ (lim ↑f, lim ↑g) ∈ t
case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
⊢ (lim ↑f, lim ↑g) ∈ t
rcases mem_uniformity_isClosed tu with ⟨d, du, dc, dt⟩
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h : d ∈ ↑f ×ˢ ↑g
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
⊢ (lim ↑f, lim ↑g) ∈ t
refine'
  H { p | (lim p.1.1, lim p.2.1) ∈ t } (CauchyFilter.mem_uniformity'.2 ⟨d, du, fun f g h => _⟩)
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h : d ∈ ↑f ×ˢ ↑g
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
rcases mem_prod_iff.1 h with ⟨x, xf, y, yg, h⟩
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
have limc : ∀ (f : CauchyFilter α), ∀ x ∈ f.1, lim f.1 ∈ closure x := by
  intro f x xf
  rw [closure_eq_cluster_pts]
  exact f.2.1.mono (le_inf f.2.le_nhds_lim (le_principal_iff.2 xf))
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure (x ×ˢ y) ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
have := dc.closure_subset_iff.2 h
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure (x ×ˢ y) ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
rw [closure_prod_eq] at this
no goals
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
refine' dt (this ⟨_, _⟩) <;> dsimp <;> apply limc <;> assumption
no goals
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
⊢ SeparatedSpace α
infer_instance
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝¹ g✝ : CauchyFilter α
H : (f✝¹, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f✝ g : CauchyFilter α
h✝ : d ∈ ↑f✝ ×ˢ ↑g
x✝ : Set α
xf✝ : x✝ ∈ ↑f✝
y : Set α
yg : y ∈ ↑g
h : x✝ ×ˢ y ⊆ d
f : CauchyFilter α
x : Set α
xf : x ∈ ↑f
⊢ lim ↑f ∈ closure x
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
⊢ ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
intro f x xf
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝¹ g✝ : CauchyFilter α
H : (f✝¹, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f✝ g : CauchyFilter α
h✝ : d ∈ ↑f✝ ×ˢ ↑g
x✝ : Set α
xf✝ : x✝ ∈ ↑f✝
y : Set α
yg : y ∈ ↑g
h : x✝ ×ˢ y ⊆ d
f : CauchyFilter α
x : Set α
xf : x ∈ ↑f
⊢ lim ↑f ∈ {a | ClusterPt a (𝓟 x)}
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝¹ g✝ : CauchyFilter α
H : (f✝¹, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f✝ g : CauchyFilter α
h✝ : d ∈ ↑f✝ ×ˢ ↑g
x✝ : Set α
xf✝ : x✝ ∈ ↑f✝
y : Set α
yg : y ∈ ↑g
h : x✝ ×ˢ y ⊆ d
f : CauchyFilter α
x : Set α
xf : x ∈ ↑f
⊢ lim ↑f ∈ closure x
rw [closure_eq_cluster_pts]
no goals
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝¹ g✝ : CauchyFilter α
H : (f✝¹, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f✝ g : CauchyFilter α
h✝ : d ∈ ↑f✝ ×ˢ ↑g
x✝ : Set α
xf✝ : x✝ ∈ ↑f✝
y : Set α
yg : y ∈ ↑g
h : x✝ ×ˢ y ⊆ d
f : CauchyFilter α
x : Set α
xf : x ∈ ↑f
⊢ lim ↑f ∈ {a | ClusterPt a (𝓟 x)}
exact f.2.1.mono (le_inf f.2.le_nhds_lim (le_principal_iff.2 xf))