neBot — Mathlib

English

If every component f i is non-bottom, then the product filter pi f is non-bottom.

Русский

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

LaTeX

$$$\\forall i,\\ NeBot\\left(f i\\right) \\Rightarrow \\ NeBot\\left(\\pi f\\right)$$$

Lean4

instance neBot [h : ∀ i, NeBot (f i ⊓ 𝓟 (s i))] {I : Set ι} : NeBot (pi f ⊓ 𝓟 (I.pi s)) :=
  (pi_inf_principal_univ_pi_neBot.2 ‹_›).mono <| inf_le_inf_left _ <| principal_mono.2 fun _ hx i _ => hx i trivial

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