coprod — Mathlib

English

Coproduct of filters. The coproduct of f : Filter α and g : Filter β is the filter on α × β given by f.comap Prod.fst ⊔ g.comap Prod.snd.

Русский

Копрообраз фильтров. Coprod(f,g) — фильтр на α×β, равный f.comap Prod.fst ⊔ g.comap Prod.snd.

LaTeX

$$$\\mathrm{coprod}(m) = f^{\\ast}(\\mathrm{Prod.fst}) \\; \\sqcup\\; g^{\\ast}(\\mathrm{Prod.snd})$$$

Lean4

/-- Coproduct of filters. -/
protected def coprod (f : Filter α) (g : Filter β) : Filter (α × β) :=
  f.comap Prod.fst ⊔ g.comap Prod.snd

Похожие утверждения