diff_union_diff_cancel' — Mathlib

English

Under more general hypotheses hi and hu on sets s,t,u, the equality (s \ t) ∪ (t \ u) = s \ u holds.

Русский

При более общих гипотезах hi и hu над множествами s,t,u выполняется равенство (s \ t) ∪ (t \ u) = s \ u.

LaTeX

$$$(s \ t) \cup (t \ u) = s \ u \text{ under } hi, hu$, where $\,hi: s \cap u \subseteq t$, $hu: t \subseteq s \cup u$.$$

Lean4

/-- A version of `diff_union_diff_cancel` with more general hypotheses. -/
theorem diff_union_diff_cancel' (hi : s ∩ u ⊆ t) (hu : t ⊆ s ∪ u) : (s \ t) ∪ (t \ u) = s \ u :=
  sdiff_sup_sdiff_cancel' hi hu

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