disjoint_union_left — Mathlib

English

Let s, t, and u be subsets of a set. Then the union of s and t is disjoint from u if and only if s is disjoint from u and t is disjoint from u.

Русский

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

LaTeX

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

Lean4

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

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