pmap — Mathlib

English

For any p and f, if certain condition holds, then Nodup(pmap f l H).

Русский

При заданных условиях, Nodup(pmap f l H).

LaTeX

$$$\\operatorname{Nodup}(\\mathrm{pmap}\\ f\\ l\\ H) $$$

Lean4

theorem pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} {H} (hf : ∀ a ha b hb, f a ha = f b hb → a = b)
    (h : Nodup l) : Nodup (pmap f l H) := by
  rw [pmap_eq_map_attach]
  exact h.attach.map fun ⟨a, ha⟩ ⟨b, hb⟩ h => by congr; exact hf a (H _ ha) b (H _ hb) h

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