image₂_inter_subset_right — Mathlib

English

image₂ f s (t ∩ t') ⊆ image₂ f s t ∩ image₂ f s t'.

Русский

image₂ f s (t ∩ t') ⊆ image₂ f s t ∩ image₂ f s t'.

LaTeX

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

Lean4

theorem image₂_inter_subset_right [DecidableEq β] : image₂ f s (t ∩ t') ⊆ image₂ f s t ∩ image₂ f s t' :=
  coe_subset.1 <| by
    push_cast
    exact image2_inter_subset_right

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