image2_swap — Mathlib

English

For any sets S ⊆ α and T ⊆ β, image2 f S T equals image2 of the swapped function on T S, i.e., { f(a,b) | a ∈ S, b ∈ T } = { f(b,a) | b ∈ T, a ∈ S }.

Русский

Для любых множеств S ⊆ α и T ⊆ β верна равенство: { f(a,b) | a ∈ S, b ∈ T } = { f(b,a) | b ∈ T, a ∈ S }.

LaTeX

$$$$\\{ f(a,b) \\mid a \\in S,\\; b \\in T \\} = \\{ f(b,a) \\mid b \\in T,\\; a \\in S \\}.$$$$

Lean4

theorem image2_swap (s : Set α) (t : Set β) : image2 f s t = image2 (fun a b => f b a) t s := by grind

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