English
The preimage of an intersection equals the intersection of preimages, provided the injectivity conditions on the pieces hold.
Русский
Предобраз пересечения равно пересечению предобразов, при соблюдении условий инъективности на соответствующих частях.
LaTeX
$$$$ \\mathrm{preimage}(s \\cap t,f,hf) = \\mathrm{preimage}(s,f,hf) \\cap \\mathrm{preimage}(t,f,ht). $$$$
Lean4
@[simp]
theorem preimage_inter [DecidableEq α] [DecidableEq β] {f : α → β} {s t : Finset β} (hs : Set.InjOn f (f ⁻¹' ↑s))
(ht : Set.InjOn f (f ⁻¹' ↑t)) :
(preimage (s ∩ t) f fun _ hx₁ _ hx₂ => hs (mem_of_mem_inter_left hx₁) (mem_of_mem_inter_left hx₂)) =
preimage s f hs ∩ preimage t f ht :=
Finset.coe_injective (by simp)
