neBot

Mathlib.Order.Filter.NAry

URI: https://scilib.ai/kg/mathlib#Filter.map₂.neBot

English

There is a construction that given NeBot f and NeBot g yields NeBot (map₂ m f g).

Русский

Существует построение: если f и g неботовы, то map₂ m f g тоже неботов.

LaTeX

$$$ [\mathrm{NeBot}\ f] [\mathrm{NeBot}\ g] \Rightarrow (map_2 m f g).\mathrm{NeBot} $$$

Lean4

instance neBot [NeBot f] [NeBot g] : NeBot (map₂ m f g) :=
  .map₂ ‹_› ‹_›

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

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

Разделы

Аффилиация

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