English
Suppose for every a ∈ s the partial application f a is injective, and the family {t.image (f a) | a ∈ s} is pairwise disjoint. Then the cardinality of t divides the cardinality of image₂ f s t.
Русский
Пусть для каждого a ∈ s отображение f a: t → ? инъективно, и множество {t.image (f a) | a ∈ s} попарно непересекаются. Тогда |t| делит |image₂ f s t|.
LaTeX
$$$\\forall s:\\ Finset\\,\\alpha, \\forall t:\\ Finset\\,\\beta, (\\forall a \\in s, Injective (f a)) \\land ((fun a \\mapsto t.image (f a)) '' s).PairwiseDisjoint id \\Rightarrow #t \\mid #(image_2 f s t)$$$
Lean4
/-- If each partial application of `f` is injective, and images of `s` under those partial
applications are disjoint (but not necessarily distinct!), then the size of `t` divides the size of
`Finset.image₂ f s t`. -/
theorem card_dvd_card_image₂_right (hf : ∀ a ∈ s, Injective (f a))
(hs : ((fun a => t.image <| f a) '' s).PairwiseDisjoint id) : #t ∣ #(image₂ f s t) := by
classical
induction s using Finset.induction with
| empty => simp
| insert a s _ ih => ?_
specialize ih (forall_of_forall_insert hf) (hs.subset <| Set.image_mono <| coe_subset.2 <| subset_insert _ _)
rw [image₂_insert_left]
by_cases h : Disjoint (image (f a) t) (image₂ f s t)
· rw [card_union_of_disjoint h]
exact Nat.dvd_add (card_image_of_injective _ <| hf _ <| mem_insert_self _ _).symm.dvd ih
simp_rw [← biUnion_image_left, disjoint_biUnion_right, not_forall] at h
obtain ⟨b, hb, h⟩ := h
rwa [union_eq_right.2]
exact
(hs.eq (Set.mem_image_of_mem _ <| mem_insert_self _ _) (Set.mem_image_of_mem _ <| mem_insert_of_mem hb)
h).trans_subset
(image_subset_image₂_right hb)
