coe_diffs — Mathlib

English

The set-theoretic representation of diffs is the image of pairs under the difference operation.

Русский

Представление диффов в виде множества равно образу пары под операцией вычитания.

LaTeX

$$$ (s \\setminus\\setminus t)^{\\uparrow} = \\mathrm{Set.image}_2 (\\setminus) s t $$$

Lean4

@[simp, norm_cast]
theorem coe_diffs : (↑(s \\ t) : Set α) = Set.image2 (· \ ·) s t :=
  coe_image₂ _ _ _

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