English
The filter product is defined as the quotient of the dependent function space a↦ε(a) by the equivalence relation f ~ g if f(a) = g(a) eventually for l-almost every a.
Русский
Произведение по фильтру — это фактор-пространство от функций a↦ε(a) по отношению эквивалентности f ≈ g, если f(a) = g(a) почти всюду по l.
LaTeX
$$$\mathrm{Product}(l,\varepsilon) = \mathrm{Quotient}(\mathrm{productSetoid}(l,\varepsilon)).$$$
Lean4
/-- Setoid used to define the filter product. This is a dependent version of
`Filter.germSetoid`. -/
def productSetoid (l : Filter α) (ε : α → Type*) : Setoid ((a : _) → ε a)
where
r f g := ∀ᶠ a in l, f a = g a
iseqv :=
⟨fun _ => Eventually.of_forall fun _ => rfl, fun h => h.mono fun _ => Eq.symm, fun h1 h2 =>
h1.congr (h2.mono fun _ hx => hx ▸ Iff.rfl)⟩
