image2_inter_right — Mathlib

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]

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