coprodᵢ — Mathlib

English

Coproduct of filters: the coproduct of a family f is the supremum of comaps along evaluation maps.

Русский

Копродукт фильтров: копродукт семейства f — верхняя грань (супремум) по отображениям проекции.

LaTeX

$$Protected def coprodᵢ (f : ∀ i, Filter (α i)) : Filter (∀ i, α i) := ⨆ i : ι, comap (eval i) (f i)$$

Lean4

/-- Coproduct of filters. -/
protected def coprodᵢ (f : ∀ i, Filter (α i)) : Filter (∀ i, α i) :=
  ⨆ i : ι, comap (eval i) (f i)

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