pmap_cons' — Mathlib

English

Opposite direction of pmap_cons: cons mapped head equals head-mapped cons.

Русский

Обратное направление к pmap_cons: отображение головы, затем конc, равно конc, затем mapping.

LaTeX

$$cons (f a ha) (v.pmap f hp) = (cons a v).pmap f (by simpa [ha])$$

Lean4

/-- Opposite direction of `Vector.pmap_cons` -/
theorem pmap_cons' {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n) (ha : p a)
    (hp : ∀ x ∈ v.toList, p x) : cons (f a ha) (v.pmap f hp) = (cons a v).pmap f (by simpa [ha]) :=
  rfl

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