X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
⊢ ∀ (ib : Set Y), ¬b ∈ ib ∧ IsClosed ib → ∃ ia, (¬a ∈ ia ∧ IsClosed ia) ∧ ∀ (x : X), x ∈ iaᶜ → f x ∈ ibᶜ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
refine'
  ⟨fun hf u hu => hf.comp hu, fun h =>
    ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 _⟩
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ ∃ ia, (¬a ∈ ia ∧ IsClosed ia) ∧ ∀ (x : X), x ∈ iaᶜ → f x ∈ sᶜ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
⊢ ∀ (ib : Set Y), ¬b ∈ ib ∧ IsClosed ib → ∃ ia, (¬a ∈ ia ∧ IsClosed ia) ∧ ∀ (x : X), x ∈ iaᶜ → f x ∈ ibᶜ
rintro s ⟨hbs, hsc⟩
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ a ∈ closure (f ⁻¹' s) → b ∈ s
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ ∃ ia, (¬a ∈ ia ∧ IsClosed ia) ∧ ∀ (x : X), x ∈ iaᶜ → f x ∈ sᶜ
refine' ⟨closure (f ⁻¹' s), ⟨mt _ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ a ∈ seqClosure (f ⁻¹' s) → b ∈ s
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ a ∈ closure (f ⁻¹' s) → b ∈ s
rw [← seqClosure_eq_closure]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
u : ℕ → X
hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s
hu : Tendsto u atTop (𝓝 a)
⊢ b ∈ s
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ a ∈ seqClosure (f ⁻¹' s) → b ∈ s
rintro ⟨u, hus, hu⟩
no goals
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
u : ℕ → X
hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s
hu : Tendsto u atTop (𝓝 a)
⊢ b ∈ s
exact hsc.mem_of_tendsto (h u hu) (eventually_of_forall hus)