English
If f is injective2, then image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t'.
Русский
Если f инъективна в двух аргументах, то образ_2 сохраняет пересечение по правой стороне: image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t'.
LaTeX
$$$\\operatorname{image}_2 f s (t \\cap t') = \\operatorname{image}_2 f s t \\cap \\operatorname{image}_2 f s t'$$$
Lean4
theorem image₂_inter_right [DecidableEq β] (hf : Injective2 f) : image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t' :=
coe_injective <| by
push_cast
exact image2_inter_right hf