prod_atBot_atBot_eq — Mathlib

English

The product of bottom filters on α and β is the bottom filter on α × β.

Русский

Произведение фильтров atBot на α и atBot на β равно atBot на α × β.

LaTeX

$$$(\\operatorname{atBot}_{\\alpha}) \\times^\\mathrm{S} (\\operatorname{atBot}_{\\beta}) = \\operatorname{atBot}_{\\alpha \\times \\beta}$$$

Lean4

theorem prod_atBot_atBot_eq [Preorder α] [Preorder β] :
    (atBot : Filter α) ×ˢ (atBot : Filter β) = (atBot : Filter (α × β)) :=
  @prod_atTop_atTop_eq αᵒᵈ βᵒᵈ _ _

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