map₂_eq_bot_iff — Mathlib

English

The product of two filters under m is the bottom filter if and only if at least one of the factors is bottom.

Русский

Произведение двух фильтров с помощью m равно нижнему фильтру тогда и только тогда, когда хотя бы один из факторов равен нижнему фильтру.

LaTeX

$$$ map_2 m f g = \bot \iff f = \bot \lor g = \bot $$$

Lean4

@[simp]
theorem map₂_eq_bot_iff : map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥ := by simp [← map_prod_eq_map₂]

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