map_mem — Mathlib

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

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