div_neBot_iff

Mathlib.Order.Filter.Pointwise

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

English

(f / g).NeBot holds if and only if f.NeBot and g.NeBot.

Русский

Свойство не пустоты делителя: (f / g).NeBot равно истине тогда, когда f.NeBot и g.NeBot.

LaTeX

$$$(f / g).NeBot \\iff (f.NeBot \\land g.NeBot).$$$

Lean4

@[to_additive (attr := simp)]
theorem div_neBot_iff : (f / g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff

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

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

Разделы

Аффилиация

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