disjoint_prod — Mathlib

English

Disjoint (s1 × t1) and (s2 × t2) is equivalent to Disjoint s1 s2 or Disjoint t1 t2.

Русский

Параллелизм множеств: Disjoint (s1 × t1) (s2 × t2) эквивалентно Disjoint s1 s2 или Disjoint t1 t2.

LaTeX

$$$ \text{Disjoint} (s_1 \times t_1) (s_2 \times t_2) \iff \text{Disjoint } s_1 s_2 \lor \text{Disjoint } t_1 t_2 $$$

Lean4

@[simp]
theorem disjoint_prod : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂ :=
  by
  simp_rw [disjoint_left, mem_prod, Prod.forall]
  grind

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