English
The dependent germ product is presented as the quotient of the set of functions a↦ε(a) by the pointwise equality almost everywhere along l.
Русский
Зависимое Жермен Продукта задаётся как фактор-множество функций a↦ε(a) по отношению ≈ почти повсюду вдоль l.
LaTeX
$$$(l : \text{Filter } \alpha)\ (\varepsilon : \alpha \to \text{Type}*)\ :\ \mathrm{Type}$ defined as $\mathrm{GermProduct}(l, \varepsilon) = \mathrm{Quotient}(\mathrm{productSetoid}(l, \varepsilon)).$$$
Lean4
/-- The filter product `(a : α) → ε a` at a filter `l`. This is a dependent version of
`Filter.Germ`. -/
def Product (l : Filter α) (ε : α → Type*) : Type _ :=
Quotient (productSetoid l ε)
