antitone — Mathlib

English

If a scheme has vanishing diameter, then for any ε>0 and any branch x, there exists n such that all pairs of points in A(res x n) are within ε in distance.

Русский

Если диаметр уменьшается вдоль ветви, то существует n, такое что любая пара точек внутри A(res x n) ближе чем ε.

LaTeX

$$$ \exists n, \forall y,z \in A(\mathrm{res}(x,n)), \; \mathrm{dist}(y,z) < ε. $$$

Lean4

protected theorem antitone [TopologicalSpace α] (hA : ClosureAntitone A) : CantorScheme.Antitone A := fun l a =>
  subset_closure.trans (hA l a)

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