disjoint_union_left — Mathlib

English

Disjoint (S ∪ T) U holds if and only if Disjoint S U and Disjoint T U.

Русский

Непересечение (S ∪ T) с U эквивалентно непересечённости S с U и непересечённости T с U.

LaTeX

$$$$ \text{Disjoint}(S \cup T, U) \;\Leftrightarrow\; \text{Disjoint}(S,U) \land \text{Disjoint}(T,U). $$$$

Lean4

@[simp]
theorem disjoint_union_left : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u := by
  simp only [disjoint_left, mem_union, or_imp, forall_and]

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