image2_inter_left — Mathlib

English

If f is 2-ary injective, then image2 preserves intersections in the first argument: image2 f (S ∩ S') T = image2 f S T ∩ image2 f S' T.

Русский

Если функция f дву-арная инъективна, то image2 сохраняет пересечение в первом аргументе: image2 f (S ∩ S') T = image2 f S T ∩ image2 f S' T.

LaTeX

$$$$\\text{If } \\mathrm{Injective2}(f),\\; \\operatorname{image2} f (S \\cap S') T = \\operatorname{image2} f S T \\cap \\operatorname{image2} f S' T.$$$$

Lean4

theorem image2_inter_left (hf : Injective2 f) : image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t := by
  simp_rw [← image_uncurry_prod, inter_prod, image_inter hf.uncurry]

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