English
If there is a mapping h such that for all a ∈ m1, b ∈ m2, r a b holds and card m1 = card m2, then Rel r m1 m2.
Русский
Если существует отображение h такое, что для всех a ∈ m1, b ∈ m2 выполняется r a b и кардиналы m1 и m2 равны, то Rel r m1 m2.
LaTeX
$$$\forall {m1 m2 : Multiset\,\alpha},\ (\forall a b, a \in m1 \to b \in m2 \to r a b) \to \operatorname{card}(m1) = \operatorname{card}(m2) \to Rel\ r\ m1\ m2$$$
Lean4
theorem rel_of_forall {m1 m2 : Multiset α} {r : α → α → Prop} (h : ∀ a b, a ∈ m1 → b ∈ m2 → r a b)
(hc : card m1 = card m2) : m1.Rel r m2 := by
revert m1
refine @(m2.induction_on ?_ ?_)
· intro m _h hc
rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
· intro a t ih m h hc
rw [card_cons] at hc
obtain ⟨b, hb⟩ := card_pos_iff_exists_mem.1 (show 0 < card m from hc.symm ▸ Nat.succ_pos _)
obtain ⟨m', rfl⟩ := exists_cons_of_mem hb
refine rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih ?_ ?_, rfl⟩
· exact fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)
· simpa using hc
