English
If for each b ∈ t the map a ↦ f a b is injective and the family {s.image (f a b) | b ∈ t} is pairwise disjoint, then #s divides #(image₂ f s t).
Русский
Если для каждого b ∈ t отображение a ↦ f a b инъективно и семейство {s.image (f a b) | b ∈ t} попарно непересекаются, то |s| делит #(image₂ f s t).
LaTeX
$$$\\forall b:\\beta, b \\in t \\Rightarrow Injective (\\lambda a, f a b) \\land ((fun b' => s.image (f · b')) '' t).PairwiseDisjoint id \\Rightarrow #s \\mid #(image_2 f s t)$$$
Lean4
/-- If each partial application of `f` is injective, and images of `t` under those partial
applications are disjoint (but not necessarily distinct!), then the size of `s` divides the size of
`Finset.image₂ f s t`. -/
theorem card_dvd_card_image₂_left (hf : ∀ b ∈ t, Injective fun a => f a b)
(ht : ((fun b => s.image fun a => f a b) '' t).PairwiseDisjoint id) : #s ∣ #(image₂ f s t) := by rw [← image₂_swap];
exact card_dvd_card_image₂_right hf ht
