pi_neBot

Mathlib.Order.Filter.Pi

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

English

NeBot (pi f) is equivalent to NeBot of every f i: NeBot (pi f) ↔ ∀ i, NeBot (f i).

Русский

NeBot(π f) эквивалентно NeBot каждого f i: NeBot(π f) ⇔ ∀ i, NeBot(f i).

LaTeX

$$$\\mathrm{NeBot}(\\pi f) \\;\\Leftrightarrow\\; \\forall i, \\mathrm{NeBot}(f i)$$$

Lean4

@[simp]
theorem pi_neBot : NeBot (pi f) ↔ ∀ i, NeBot (f i) := by simp [neBot_iff]

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

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

Разделы

Аффилиация

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