English
Let m be a multiset, a an element, r a binary relation on α, and n ∈ ℕ. Then (replicate n a) Rel r m holds exactly when card m = n and every element x ∈ m satisfies r(a,x).
Русский
Пусть m — мультисет, a — элемент, r — бинарное отношение на α, и n ∈ ℕ. Тогда (replicate n a) Rel r m эквивалентно тому, что card m = n и для каждого x ∈ m выполняется r(a,x).
LaTeX
$$$$ (\\operatorname{replicate} n a) \\operatorname{Rel}_{r} m \\iff \\operatorname{card}(m) = n \\wedge \\forall x \\in m,\\ r(a,x). $$$$
Lean4
theorem rel_replicate_left {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :
(replicate n a).Rel r m ↔ card m = n ∧ ∀ x, x ∈ m → r a x :=
⟨fun h =>
⟨(card_eq_card_of_rel h).symm.trans (card_replicate _ _), fun x hx =>
by
obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx
rwa [eq_of_mem_replicate hb1] at hb2⟩,
fun h =>
rel_of_forall (fun _ _ hx hy => (eq_of_mem_replicate hx).symm ▸ h.2 _ hy) (Eq.trans (card_replicate _ _) h.1.symm)⟩
