English
If f is injective on s ∪ t, then the image of (s ∩ t) under f equals the intersection of the images: (s ∩ t).image f = s.image f ∩ t.image f.
Русский
Если f инъективна на объединении s и t, то образ пересечения равен пересечению образов: (s ∩ t).image f = s.image f ∩ t.image f.
LaTeX
$$$(\,s \cap t\,).image f = s.image f \cap t.image f$ (при условии, что hf : \text{Set.InjOn } f (s \cup t))$$$
Lean4
theorem image_inter_of_injOn [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Set.InjOn f (s ∪ t)) :
(s ∩ t).image f = s.image f ∩ t.image f :=
coe_injective <| by
push_cast
exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb