vsub

Mathlib.Order.Filter.Pointwise

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

English

If f and g are nontrivial filters on β, then the vector-subtracted filter f -ᵥ g is a nontrivial filter on α.

Русский

Пусть f и g — ненулевые фильтры на β. Тогда фильтр f -ᵥ g над α тоже ненулевой.

LaTeX

$$$(f \ne \bot) \land (g \ne \bot) \Rightarrow (f -\!\!_v g) \ne \bot$$$

Lean4

protected theorem vsub : NeBot f → NeBot g → NeBot (f -ᵥ g) :=
  NeBot.map₂

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

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

Разделы

Аффилиация

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