English
Fix a ∈ α and suppose f a is injective. Then the image over the intersection distributes over intersection: image₂ f {a} (t1 ∩ t2) = image₂ f {a} t1 ∩ image₂ f {a} t2.
Русский
Пусть a фиксировано и f(a) инъективна. Тогда образ над пересечением множеств распределяется по пересечениям: image₂ f {a} (t1 ∩ t2) = image₂ f {a} t1 ∩ image₂ f {a} t2.
LaTeX
$$$(Injective\ (f\ a)) \Rightarrow \mathrm{image}_2\ f\{a\}(t_1 \cap t_2) = \mathrm{image}_2\ f\{a\} t_1 \cap \mathrm{image}_2\ f\{a\} t_2$$$
Lean4
theorem image₂_singleton_inter [DecidableEq β] (t₁ t₂ : Finset β) (hf : Injective (f a)) :
image₂ f { a } (t₁ ∩ t₂) = image₂ f { a } t₁ ∩ image₂ f { a } t₂ := by
simp_rw [image₂_singleton_left, image_inter _ _ hf]
