English
Membership in map and bind versions of pi-type is characterized by existence of witnesses in the domain and appropriate equalities in the codomain.
Русский
Принадлежность к отображенного/связного Pi-множества описывается существованием свидетелей и соответствующими равенствами в кодоможноcти.
LaTeX
$$$f \\in \\mathrm{map}\\ f\\ s \\iff \\exists a\\in s, \\ f(a) = b$ и аналогично для \\mathrm{bind}.$$
Lean4
protected theorem pi {s : Multiset α} {t : ∀ a, Multiset (β a)} : Nodup s → (∀ a ∈ s, Nodup (t a)) → Nodup (pi s t) :=
Multiset.induction_on s (fun _ _ => nodup_singleton _)
(by
intro a s ih hs ht
have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1
have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2
simp only [pi_cons, nodup_bind]
refine ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has), ?_⟩
refine (ht a <| mem_cons_self _ _).pairwise ?_
exact fun b₁ _ b₂ _ neb =>
disjoint_map_map.2 fun f _ g _ eq =>
have : Pi.cons s a b₁ f a (mem_cons_self _ _) = Pi.cons s a b₂ g a (mem_cons_self _ _) := by rw [eq]
neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this)
