instNeBotForallPi

Mathlib.Order.Filter.Pi

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

English

If each f i is NeBot, then the product Pi-filter pi f is NeBot.

Русский

Если каждый f i непротиворечив, то произведение фильтров π f тоже непустой ( NeBot ).

LaTeX

$$$[\\forall i, (f i).NeBot] \\Rightarrow (\\pi f).NeBot$$$

Lean4

instance [∀ i, NeBot (f i)] : NeBot (pi f) :=
  pi_neBot.2 ‹_›

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

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

Разделы

Аффилиация

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