Theorems · Definition · general topology

RestrictedProduct

{ι : Type u_1} → (R : ι → Type u_2) → ((i : ι) → Set (R i)) → Filter ι → Type (max u_1 u_2)

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.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

117 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 13 definitions · uses no axioms