image₂_inter_union_subset_union

English

For any f: α × β → γ and Finsets s,s' ⊆ α, t,t' ⊆ β, the image₂ of the intersection with the union is contained in the union of image₂s: image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t'.

Русский

Для любых f: α×β→γ и Finsets s, s' ⊆ α, t, t' ⊆ β, имеет место image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t'.

LaTeX

$$$\\forall s,t,s',t' : Finset\\,\\alpha, Finset\\,\\beta, image_2 f (s \\cap s') (t \\cup t') \\subseteq image_2 f s t \\cup image_2 f s' t'$$$

Lean4

theorem image₂_inter_union_subset_union : image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t' :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_inter_union_subset_union

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