eraseIdx_pmap — Mathlib

English

Erasing an index and then pmapping is the same as pmapping with a mapped erase.

Русский

Удаление индекса, затем отображение через pmap, эквивалентно отображению с удалением по отображению.

LaTeX

$$$\\text{eraseIdx\_pmap}(f, l, hl, n) = \\text{pmap } f (l.eraseIdx n) (\\cdot)$$$

Lean4

theorem eraseIdx_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (hl : ∀ a ∈ l, p a) (n : ℕ) :
    (pmap f l hl).eraseIdx n = (l.eraseIdx n).pmap f fun a ha ↦ hl a (eraseIdx_subset ha) :=
  match l, hl, n with
  | [], _, _ => rfl
  | a :: _, _, 0 => rfl
  | a :: as, h, n + 1 => by rw [forall_mem_cons] at h; simp [eraseIdx_pmap f h.2 n]

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