image2_inter_union_subset_union — Mathlib

English

Let f be a function on pairs; then image2 f (s ∪ s') (t ∩ t') is contained in image2 f s t ∪ image2 f s' t'.

Русский

Пусть f определяется на парах; тогда image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'.

LaTeX

$$$\\operatorname{image}_2 f (s \\cup s') (t \\cap t') \\subseteq \\operatorname{image}_2 f s t \\cup \\operatorname{image}_2 f s' t'$$$

Lean4

theorem image2_inter_union_subset_union : image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t' :=
  by
  rw [image2_union_right]
  exact union_subset_union (image2_subset_right inter_subset_left) (image2_subset_right inter_subset_right)

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