cobounded_prod — Mathlib

English

The cobounded filter on α×β is the coprod of the cobounded filters on α and β.

Русский

Фильтр кобундированности на α×β равен coproduct кобундированных фильтров на α и β.

LaTeX

$$$\operatorname{cobounded}(\alpha\times\beta) = (\operatorname{cobounded}\alpha)\;\text{coprod}\; (\operatorname{cobounded}\beta)$$$

Lean4

theorem cobounded_prod : cobounded (α × β) = (cobounded α).coprod (cobounded β) :=
  rfl

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