English
If f is 2-ary injective, then image2 preserves intersections in the second argument: image2 f S (T ∩ T') = image2 f S T ∩ image2 f S T'.
Русский
Если функция f дву-арная инъективна, то image2 сохраняет пересечение во втором аргументе: image2 f S (T ∩ T') = image2 f S T ∩ image2 f S T'.
LaTeX
$$$$\\operatorname{image2} f S (T \\cap T') = \\operatorname{image2} f S T \\cap \\operatorname{image2} f S T'.$$$$
Lean4
theorem image2_inter_right (hf : Injective2 f) : image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t' := by
simp_rw [← image_uncurry_prod, prod_inter, image_inter hf.uncurry]