seq — Mathlib

English

Given a Cauchy f and a sequence U, seq(n) is a chosen element of setSeq(n) for each n.

Русский

Пусть дан сформированный Cauchy-фильтр f и последовательность U; для каждого n выбрано элемент seq(n) из setSeq(n).

LaTeX

$$$\text{seq}(n) \in \text{setSeq}(hf,U_{mem},n)$$$

Lean4

/-- A sequence of points such that `seq n ∈ setSeq n`. Here `setSeq` is an antitone
sequence of sets `setSeq n ∈ f` with diameters controlled by a given sequence
of entourages. -/
def seq (n : ℕ) : α :=
  (hf.1.nonempty_of_mem (setSeq_mem hf U_mem n)).choose

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