image₂_inter_union_subset — Mathlib

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

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