English
If the preimage {a | a ∈ m} is Pairwise with respect to the relation r after applying f, then {b | b ∈ m.map f} is Pairwise with respect to r.
Русский
Если множество предобразов {a | a ∈ m} попарно удовлетворяет relation r после применения f, то множество изображенных элементов {b | b ∈ m.map f} попарно удовлетворяет r.
LaTeX
$${a | a ∈ m}.Pairwise (λ a1 a2 => r (f a1) (f a2)) \\Rightarrow {b | b ∈ m.map f}.Pairwise r$$
Lean4
theorem map_set_pairwise {f : α → β} {r : β → β → Prop} {m : Multiset α}
(h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)) : {b | b ∈ m.map f}.Pairwise r := fun b₁ h₁ b₂ h₂ hn =>
by
obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂
exact h H₁ H₂ (mt (congr_arg f) hn)
