English
image₂ f (s ∪ t) (s ∩ t) ⊆ image₂ f s t, assuming f is symmetric in its two arguments.
Русский
image₂ f (s ∪ t) (s ∩ t) ⊆ image₂ f s t при симметричной конструкции f.
LaTeX
$$$\\forall s,t:\\ Finset\\,\\alpha,\\, (\\forall a,b, f a b = f b a) \\Rightarrow image_2 f (s \\cup t) (s \\cap t) \\subseteq image_2 f s t$$$
Lean4
theorem image₂_inter_union_subset {f : α → α → β} {s t : Finset α} (hf : ∀ a b, f a b = f b a) :
image₂ f (s ∩ t) (s ∪ t) ⊆ image₂ f s t :=
coe_subset.1 <| by
push_cast
exact image2_inter_union_subset hf