disjoint_product — Mathlib

English

Disjointness of a product is equivalent to disjointness of factors: Disjoint (s × t) (s' × t') ⇔ Disjoint s s' ∨ Disjoint t t'.

Русский

Непересечение произведения эквивалентно непересечению факторов: Disjoint (s × t) (s' × t') ⇔ Disjoint s s' ∨ Disjoint t t'.

LaTeX

$$$\\operatorname{Disjoint}(s \\times t, s' \\times t') \\iff (\\operatorname{Disjoint}(s,s') \\lor \\operatorname{Disjoint}(t,t'))$$$

Lean4

theorem disjoint_product : Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t' := by
  simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]

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