diffs — Mathlib

English

Diffs is defined as the image of a pair under the binary operation, i.e., the Finset of all a \\ b with a ∈ s and b ∈ t.

Русский

Diffs определяется как образ пары под бинарной операцией; т.е. конечный набор всех a \\ b, где a ∈ s и b ∈ t.

LaTeX

$$$ \\mathrm{diffs}(s,t) = \\operatorname{image}_2 (\\setminus) (s,t) $$$

Lean4

/-- `s \\ t` is the finset of elements of the form `a \ b` where `a ∈ s`, `b ∈ t`. -/
def diffs : Finset α → Finset α → Finset α :=
  image₂ (· \ ·)

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