prod_atTop_atTop_eq — Mathlib

English

For Preorder α, β, the product of the atTop filters on α and β equals atTop on α × β.

Русский

Для частично упорядочиваемых множеств, произведение фильтров atTop на α и atTop на β равно atTop на α × β.

LaTeX

$$$(atTop : Filter\\, α) \\timesˢ (atTop : Filter\\, β) = (atTop : Filter\\, (α \\times β))$$$

Lean4

theorem prod_atTop_atTop_eq [Preorder α] [Preorder β] :
    (atTop : Filter α) ×ˢ (atTop : Filter β) = (atTop : Filter (α × β)) :=
  by
  cases isEmpty_or_nonempty α
  · subsingleton
  cases isEmpty_or_nonempty β
  · subsingleton
  simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm

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