English
Given a starting point p and a countable family of cofinal subsets 𝒟 indexed by ι, define a sequence s by s(0) = p and s(n+1) = (𝒟 i).above (s(n)) where i is obtained from decoding n; this yields an increasing sequence intersecting every 𝒟 i.
Русский
Дано начальное p и счётную семью кофинальных подмножеств 𝒟, индексируемую ι. Определим последовательность s: s(0)=p, s(n+1) = (𝒟 i).above(s(n)), где i — получено при декодировании n; полученная последовательность возрастает и пересекает каждое 𝒟 i.
LaTeX
$$$ \text{sequenceOfCofinals}(p,\mathcal{D}) : \mathbb{N} \to P \quad\text{с$$
Lean4
/-- Given a starting point, and a countable family of cofinal sets,
this is an increasing sequence that intersects each cofinal set. -/
noncomputable def sequenceOfCofinals : ℕ → P
| 0 => p
| n + 1 =>
match Encodable.decode n with
| none => sequenceOfCofinals n
| some i => (𝒟 i).above (sequenceOfCofinals n)
