frechetUrysohnSpace — Mathlib

English

If f: X → Y is an inducing map and Y is Frechet-Urysohn, then X is Frechet-Urysohn.

Русский

Если f: X → Y индуктивно отображает X в Y и Y является пространством Фреше–Ури́шхо́н, то и X таким является.

LaTeX

$$$\text{IsInducing}(f) \Rightarrow \text{FrechetUrysohnSpace}(X)$ (при условии $\text{FrechetUrysohnSpace}(Y)$)$$

Lean4

theorem frechetUrysohnSpace [FrechetUrysohnSpace Y] {f : X → Y} (hf : IsInducing f) : FrechetUrysohnSpace X :=
  by
  refine ⟨fun s x hx ↦ ?_⟩
  rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx
  rcases hx with ⟨u, hus, hu⟩
  choose v hv hvu using hus
  refine ⟨v, hv, ?_⟩
  simpa only [hf.tendsto_nhds_iff, Function.comp_def, hvu]

Похожие утверждения