instNeBot

Mathlib.Order.Filter.Prod

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

English

There is an instance saying: if f and g are NeBot, then f × g is NeBot.

Русский

Существует инстанс: если f и g неботовы, то их произведение неботово.

LaTeX

$$$ [\\text{hf : NeBot f}] [\\text{hg : NeBot g}] : \\mathrm{NeBot} (f \\times\\! g) $$$

Lean4

instance instNeBot [hf : NeBot f] [hg : NeBot g] : NeBot (f ×ˢ g) :=
  hf.prod hg

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

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

Разделы

Аффилиация

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