English
The restricted product of a family R_i relative to subsets A_i and a filter F consists of all tuples x_i ∈ R_i such that the set {i | x_i ∈ A_i} lies in F.
Русский
Ограниченное произведение семейства пространств R_i относительно подмножеств A_i и фильтра F есть набор всех кортежей x_i ∈ R_i, для которых множество {i | x_i ∈ A_i} принадлежит F.
LaTeX
$$$\\mathrm{RestrictedProduct}(\\mathcal{F}) = \\{ x : \\prod_i R_i \\;|\\; \\{ i \\mid x_i \\in A_i \\} \\in \\mathcal{F} \\}.$$$
Lean4
/-- The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.
The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.
Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`. -/
def RestrictedProduct (𝓕 : Filter ι) : Type _ :=
{ x : Π i, R i // ∀ᶠ i in 𝓕, x i ∈ A i }
