English
Let f: α × α → β satisfy f(a,b) = f(b,a) for all a,b. Then for any sets s,t ⊆ α, the image of the pair (s ∩ t, s ∪ t) under f is contained in the image of (s,t): image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t.
Русский
Пусть f: α × α → β удовлетворяет f(a,b) = f(b,a) для всех a,b. Тогда для любых подмножеств s,t ⊆ α множества значений f(a,b) с a ∈ s ∩ t и b ∈ s ∪ t лежит в множестве значений f(a,b) с a ∈ s и b ∈ t.
LaTeX
$$$\\bigl(\\forall a,b,\\ f(a,b)=f(b,a)\\bigr) \\Rightarrow \\{ f(a,b) \\mid a \\in s \\cap t,\\ b \\in s \\cup t \\} \\subseteq \\{ f(a,b) \\mid a \\in s,\\ b \\in t \\}$$$
Lean4
theorem image2_inter_union_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) :
image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t := by
rw [inter_comm]
exact image2_inter_union_subset_union.trans (union_subset (image2_comm hf).subset Subset.rfl)
