sdiff_union_sdiff_cancel — Mathlib

English

Let t be a subset of s and u be a subset of t. Then the union of the relative complements (s \ t) and (t \ u) equals the relative complement (s \ u).

Русский

Пусть t ⊆ s и u ⊆ t. Тогда объединение частных различий s \ t и t \ u равно сдвигу s \ u.

LaTeX

$$$ (t \subseteq s) \land (u \subseteq t) \implies (s \ t) \cup (t \ u) = (s \ u) $$$

Lean4

theorem sdiff_union_sdiff_cancel (hts : t ⊆ s) (hut : u ⊆ t) : s \ t ∪ t \ u = s \ u :=
  sdiff_sup_sdiff_cancel hts hut

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