compl_diagonal_mem_prod — Mathlib

English

The complement of the diagonal belongs to the product of l1 and l2 iff l1 and l2 are disjoint.

Русский

Комплемент диагонали принадлежит произведению фильтров l1 и l2 тогда и только тогда, когда l1 и l2 несовмещаются (Disjoint).

LaTeX

$$$(\\mathrm{diagonal}(\\alpha))^{c} \\in l_1 \\timesˢ l_2 \\iff \\mathrm{Disjoint}(l_1,l_2)$$$

Lean4

@[simp]
theorem compl_diagonal_mem_prod {l₁ l₂ : Filter α} : (diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂ := by
  simp only [mem_prod_iff, Filter.disjoint_iff, prod_subset_compl_diagonal_iff_disjoint]

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