disjoint_union_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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