image₂_union_inter_subset — Mathlib

English

General version of the previous lemma; with symmetry, image₂ f (s ∪ t) (s ∩ t) ⊆ image₂ f s t.

Русский

Обобщённая версия: image₂ f (s ∪ t) (s ∩ t) ⊆ image₂ f s t.

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₂_union_inter_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_union_inter_subset hf

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