English
From a β-scheme A on α, one obtains a partial map from (ℕ → β) to α by selecting an element from the intersection along the branch defined by a sequence.
Русский
Из β-диапазона A на α получается частичная отображение от (ℕ → β) в α, выбирая элемент из пересечения вдоль ветви, заданной последовательностью.
LaTeX
$$$ \mathrm{inducedMap}(A) : \Sigma s \subseteq (\mathbb{N} \to \beta), s \to \alpha, \text{ со значением в } \bigcap_n A(\mathrm{res}(s,n)). $$$
Lean4
/-- From a `β`-scheme on `α` `A`, we define a partial function from `(ℕ → β)` to `α`
which sends each infinite sequence `x` to an element of the intersection along the
branch corresponding to `x`, if it exists.
We call this the map induced by the scheme. -/
noncomputable def inducedMap : Σ s : Set (ℕ → β), s → α :=
⟨fun x => Set.Nonempty (⋂ n : ℕ, A (res x n)), fun x => x.property.some⟩
