mem_diffs — Mathlib

English

The coercion of the diffs set to a Set equals the two-variable image: (s \\ t)↑ = Set.image₂ (\\setminus) s t.

Русский

Приведение множества диффов к множеству равно образу Set.image₂ (\\setminus) над парами (s,t).

LaTeX

$$$ (\\uparrow (s \\\\ t) : Set \\alpha) = \\operatorname{Set.image}_2 (\\setminus) s t $$$

Lean4

@[simp]
theorem mem_diffs : c ∈ s \\ t ↔ ∃ a ∈ s, ∃ b ∈ t, a \ b = c := by simp [(· \\ ·)]

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