map_le_map_iff — Mathlib

English

If f is injective, mapping multisets by f preserves the order: mapping s and t by f yields s ≤ t iff their images satisfy the same order.

Русский

Если f инъективно, отображение мультисетов через f сохраняет порядок: $s \\le t$ тогда и только тогда, когда их образы удовлетворяют тому же порядку.

LaTeX

$$$ s.map f \\le t.map f \\iff s \\le t \\quad \\text{for } f \\text{ injective}$$$

Lean4

@[simp]
theorem map_le_map_iff {f : α → β} (hf : Function.Injective f) {s t : Multiset α} : s.map f ≤ t.map f ↔ s ≤ t := by
  classical
  refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩
  simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)

Похожие утверждения