Theorems · Theorem · order theory

Multiset.map_set_pairwise

∀ {α : Type u_1} {β : Type v} {f : α → β} {r : β → β → Prop} {m : Multiset α},
  ({a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)) → {b | b ∈ Multiset.map f m}.Pairwise r

Defined in

Mathlib.Data.Multiset.UnionInter

Cited by

4 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound