English
A function f from an index set converges to z in Z iff its projection converges to proj(z) and the fiber components converge in the total fibers.
Русский
Предел f x → z в Z эквивалентен тому, что proj ∘ f converge к proj(z) и соответствующие волокна сходятся к e(z).2.
LaTeX
$$$ Tendsto\ f\ l\ (nhds\ z) \;\iff\; ( Tendsto\ (proj \circ f)\ l\ (nhds\ (proj\ z)) \;\land\; Tendsto\ (\lambda x. (e (f x)).2)\ l\ (nhds\ (e z).2) ) $$$
Lean4
theorem tendsto_nhds_iff {α : Type*} {l : Filter α} {f : α → Z} {z : Z} (hz : z ∈ e.source) :
Tendsto f l (𝓝 z) ↔ Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (e (f x)).2) l (𝓝 (e z).2) :=
by
rw [e.nhds_eq_comap_inf_principal hz, tendsto_inf, tendsto_comap_iff, Prod.tendsto_iff, coe_coe, tendsto_principal,
coe_fst _ hz]
by_cases hl : ∀ᶠ x in l, f x ∈ e.source
· simp only [hl, and_true]
refine (tendsto_congr' ?_).and Iff.rfl
exact hl.mono fun x ↦ e.coe_fst
· simp only [hl, and_false, false_iff, not_and]
rw [e.source_eq] at hl hz
exact fun h _ ↦ hl <| h <| e.open_baseSet.mem_nhds hz
