image₂_union_inter_subset_union

English

A variant of the previous union-intersection inclusion: image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t'.

Русский

Вариант включения: image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t'.

LaTeX

$$$ image_2 f (s \\cap s') (t \\cup t') \\subseteq image_2 f s t \\cup image_2 f s' t' $$$

Lean4

theorem image₂_union_inter_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_union_inter_subset_union

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