disjoint_union_right — Mathlib

English

Let s, t, and u be subsets of a set. Then the disjointness of s with the union of t and u is equivalent to the disjointness of s with t and with u separately.

Русский

Пусть s, t и u — подмножества множества. Тогда несовместность s и (t ∪ u) эквивалентна несовместности s с t и несовместности s с u по отдельности.

LaTeX

$$$Disjoint(s, t \cup u) \iff (Disjoint(s,t) \land Disjoint(s,u))$$$

Lean4

@[simp]
theorem disjoint_union_right : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u :=
  disjoint_sup_right

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