setSeq — Mathlib

English

antitone sequence defined by intersections of the previous auxiliary sets: s_n = ⋂_{m≤n} setSeqAux m.

Русский

антизатирующая последовательность: s_n — пересечение предыдущих вспомогательных множеств.

LaTeX

$$$\text{setSeq}(n) = \bigcap_{m \le n} \bigl(\text{setSeqAux}(m)\bigr).$$$

Lean4

/-- Given a Cauchy filter `f` and a sequence `U` of entourages, `set_seq` provides
an antitone sequence of sets `s n ∈ f` such that `s n ×ˢ s n ⊆ U`. -/
def setSeq (n : ℕ) : Set α :=
  ⋂ m ∈ Set.Iic n, (setSeqAux hf U_mem m).val

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