English
If a space X has the property that for every predicate f: X → Prop, whenever every sequence converging to a is mapped by f to a convergent value f(a), then f is continuous at a, then X is a Frechet-Urysohn space.
Русский
Если пространство X обладает свойством: для каждого предиката f: X → {True, False}, если для каждой последовательности x_n → a выполняется, что f(x_n) сходится к f(a), то f непрерывна в a, тогда X является пространством Фреше–Ури́шхо́н.
LaTeX
$$(∀ f:X→Prop)(∀ a∈X, ((∀ u:ℕ→X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a)) → FrechetUrysohnSpace X$$
Lean4
/-- An alternative construction for `FrechetUrysohnSpace`: if sequential convergence implies
convergence, then the space is a Fréchet-Urysohn space. -/
theorem of_seq_tendsto_imp_tendsto
(h :
∀ (f : X → Prop) (a : X),
(∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a) :
FrechetUrysohnSpace X := by
refine ⟨fun s x hcx => ?_⟩
by_cases hx : x ∈ s
· exact subset_seqClosure hx
· obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s := by
simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,
← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true, not_true_eq_false] using
h (· ∉ s) x
rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩
exact
⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩
-- see Note [lower instance priority]
