setSeqAux — Mathlib

English

An auxiliary sequence of sets approximating a Cauchy filter: for each n, s ∈ f and s × s ⊆ U n.

Русский

Вспомогательная последовательность множеств, приближающих фильтр Коши: для каждого n существует s ∈ f с s × s ⊆ U n.

LaTeX

$${ s : Set α // s ∈ f ∧ s ×ˢ s ⊆ U n }$$

Lean4

/-- An auxiliary sequence of sets approximating a Cauchy filter. -/
def setSeqAux (n : ℕ) : { s : Set α // s ∈ f ∧ s ×ˢ s ⊆ U n } :=
  Classical.indefiniteDescription _ <| (cauchy_iff.1 hf).2 (U n) (U_mem n)

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