X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
⊢ x ∈ seqClosure s
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X
refine ⟨fun s x hcx => ?_⟩
case pos
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∈ s
⊢ x ∈ seqClosure s

case neg
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
⊢ x ∈ seqClosure s
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
⊢ x ∈ seqClosure s
by_cases hx : x ∈ s
no goals
case pos
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∈ s
⊢ x ∈ seqClosure s
exact subset_seqClosure hx
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
⊢ ∃ u, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ (x : ?m.5138) in atTop, u x ∈ s

case neg.intro.intro
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
u : ?m.5138 → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ?m.5138) in atTop, u x ∈ s
⊢ x ∈ seqClosure s
case neg
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
⊢ x ∈ seqClosure s
obtain ⟨u, hux, hus⟩ : ∃ u, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s
case neg.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s
case neg.intro.intro
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
⊢ x ∈ seqClosure s
rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩
no goals
case neg.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.4450
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s
exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩