prod_eq_bot — Mathlib

English

The product filter f × g equals the bottom filter ⊥ if and only if either f = ⊥ or g = ⊥.

Русский

Произведение фильтров равно нулю тогда и только тогда, когда либо один из них равен нулю.

LaTeX

$$$ f \\times\\! g = \\bot \\iff f = \\bot \\lor g = \\bot $$$

Lean4

@[simp]
theorem prod_eq_bot : f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥ := by
  simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop, Subtype.exists',
    exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]

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