English
Any CauSeq in a normed field converges to its limit with respect to the induced metric.
Русский
Любой CauSeq в нормированном поле сходится к своему пределу по соответствующей метрике.
LaTeX
$$$ \text{Tendsto}(\text{CauSeq}.val)\; (\text{atTop})\; (\mathcal{nhds}(\text{lim})) $$$
Lean4
/-- A scheme with vanishing diameter along each branch induces a continuous map. -/
theorem map_continuous [TopologicalSpace β] [DiscreteTopology β] (hA : VanishingDiam A) : Continuous (inducedMap A).2 :=
by
rw [Metric.continuous_iff']
rintro ⟨x, hx⟩ ε ε_pos
obtain ⟨n, hn⟩ := hA.dist_lt _ ε_pos x
rw [_root_.eventually_nhds_iff]
refine ⟨(↑) ⁻¹' cylinder x n, ?_, ?_, by simp⟩
· rintro ⟨y, hy⟩ hyx
rw [mem_preimage, Subtype.coe_mk, cylinder_eq_res, mem_setOf] at hyx
apply hn
· rw [← hyx]
apply map_mem
apply map_mem
apply continuous_subtype_val.isOpen_preimage
apply isOpen_cylinder
