prod

Mathlib.Order.Filter.Prod

URI: https://scilib.ai/kg/mathlib#Filter.NeBot.prod

English

In the filtered universe, the product of two NeBot filters is NeBot.

Русский

В рамках теории фильтров произведение двух неботовых фильтров также неботово.

LaTeX

$$$ f \\text{ NeBot } \\land g \\text{ NeBot } \\Rightarrow (f \\times\\! g) \\text{ NeBot } $$$

Lean4

protected theorem prod (hf : NeBot f) (hg : NeBot g) : NeBot (f ×ˢ g) :=
  prod_neBot.2 ⟨hf, hg⟩

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

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

Разделы

Аффилиация

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