instNeBot

Mathlib.Order.Filter.Pointwise

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

English

If f and g are nontrivial filters on β, then their vsub f -ᵥ g is nontrivial.

Русский

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

LaTeX

$$$ NeBot(f) \land NeBot(g) \Rightarrow NeBot(f -ᵥ g)$$$

Lean4

theorem instNeBot [NeBot f] [NeBot g] : NeBot (f -ᵥ g) :=
  .vsub ‹_› ‹_›

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

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

Разделы

Аффилиация

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