div

Mathlib.Order.Filter.Pointwise

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

English

If f and g are NeBot, then f / g is NeBot.

Русский

Если f и g неисчипаны, то f / g неисчипано.

LaTeX

$$$\\text{NeBot}(f) \\land \\text{NeBot}(g) \\Rightarrow \\text{NeBot}(f / g).$$$

Lean4

@[to_additive]
protected theorem div : NeBot f → NeBot g → NeBot (f / g) :=
  NeBot.map₂

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

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

Разделы

Аффилиация

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