pi_eq_bot — Mathlib

English

The product filter pi f equals the bottom filter if and only if some component is bottom; equivalently, pi f = ⊥ iff ∃ i, f i = ⊥.

Русский

Произведение фильтров π f равно нижнему фильтру тогда и только тогда, когда какой-то компонент является нижним; эквивалентно π f = ⊥ тогда и только тогда, ∃ i, f i = ⊥.

LaTeX

$$$\\pi f = \\bot \\iff \\exists i, f i = \\bot$$$

Lean4

@[simp]
theorem pi_eq_bot : pi f = ⊥ ↔ ∃ i, f i = ⊥ := by simpa using @pi_inf_principal_univ_pi_eq_bot ι α f fun _ => univ

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