English
A scheme has vanishing diameter if, along every branch, the diameters of the corresponding sets tend to 0.
Русский
Схема имеет исчезающе малую диаметр вдоль каждой ветви: диаметр множества на уровне n сходится к 0.
LaTeX
$$$ \forall x: \mathbb{N} \to \beta, \; \mathrm{Tendsto}(n \mapsto \mathrm{diam}(A(\mathrm{res}(x,n))))\; atTop\; (\mathcal{N}_0). $$$
Lean4
/-- If `x` is in the domain of the induced map of a scheme `A`,
its image under this map is in each set along the corresponding branch. -/
theorem map_mem (x : (inducedMap A).1) (n : ℕ) : (inducedMap A).2 x ∈ A (res x n) :=
by
have := x.property.some_mem
rw [mem_iInter] at this
exact this n