one_prod_one

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.one_prod_one

English

The product of unit filters on α and β is the unit filter on α×β: (1 : Filter α) ×ˢ (1 : Filter β) = 1.

Русский

Произведение единичных фильтров на α и β даёт единичный фильтр на α×β.

LaTeX

$$$(1 : Filter \\alpha) \\timesˢ (1 : Filter β) = 1$$$

Lean4

@[to_additive zero_prod_zero]
theorem one_prod_one [One β] : (1 : Filter α) ×ˢ (1 : Filter β) = 1 :=
  prod_pure_pure

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru