image2_union_inter_subset_union — Mathlib

English

Another variant: image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'.

Русский

Другая вариация: 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_union_inter_subset_union : image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t' :=
  by
  rw [image2_union_left]
  exact union_subset_union (image2_subset_left inter_subset_left) (image2_subset_left inter_subset_right)

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