disjoint_prod — Mathlib

English

Disjointness distributes over product: Disjoint (f × g) (f' × g') iff Disjoint f f' or Disjoint g g'.

Русский

Непересечение распространяется на произведение: Disjoint (f × g) (f' × g') ⇔ Disjoint f f' ∨ Disjoint g g'.

LaTeX

$$$ \\operatorname{Disjoint} (f \\times\\! g) (f' \\times\\! g') \\iff \\operatorname{Disjoint} f f' \\lor \\operatorname{Disjoint} g g' $$$

Lean4

@[simp]
theorem disjoint_prod {f' : Filter α} {g' : Filter β} : Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g' :=
  by simp only [disjoint_iff, prod_inf_prod, prod_eq_bot]

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