image2_union_inter_subset — Mathlib

English

Let f: α × α → β satisfy f(a,b) = f(b,a) for all a,b. Then image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t.

Русский

Пусть f: α × α → β удовлетворяет f(a,b) = f(b,a) для всех a,b. Тогда image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t.

LaTeX

$$$\\bigl(\\forall a,b,\\ f(a,b)=f(b,a)\\bigr) \\Rightarrow \\{ f(a,b) \\mid a \\in s \\cup t,\\ b \\in s \\cap t \\} \\subseteq \\{ f(a,b) \\mid a \\in s,\\ b \\in t \\}$$$

Lean4

theorem image2_union_inter_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 [image2_comm hf]
  exact image2_inter_union_subset hf

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