symmDiff_congr — Mathlib

English

If S Δ T is finite, then (S Δ U) finite iff (T Δ U) finite.

Русский

Если S Δ T конечна, то S Δ U конечна тогда и только тогда, когда T Δ U конечна.

LaTeX

$$$ (S\Delta T).Finite \rightarrow (S\Delta U).Finite \leftrightarrow (T\Delta U).Finite $$$

Lean4

theorem symmDiff_congr (hst : (s ∆ t).Finite) : (s ∆ u).Finite ↔ (t ∆ u).Finite
    where
  mp hsu := (hst.union hsu).subset (symmDiff_comm s t ▸ symmDiff_triangle ..)
  mpr htu := (hst.union htu).subset (symmDiff_triangle ..)

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