pmap_map — Mathlib

English

A similar compatibility holds when applying pmap after map; the result equals pmap with an adjusted predicate on the mapped elements.

Русский

Аналогичная совместимость сохраняется при применении pmap после map; результат равен pmap с корректированным предикатом на отображённые элементы.

LaTeX

$$$\text{pmap } f (\text{map } g xs) H = \text{pmap } (\lambda x hx. f(x, hx)) xs (by ...) $$$

Lean4

theorem pmap_map {p : β → Prop} (f₁ : (b : β) → p b → γ) (f₂ : α → β) (H : ∀ x ∈ (xs.map f₂).toList, p x) :
    pmap f₁ (map f₂ xs) H = pmap (fun x hx => f₁ (f₂ x) hx) xs (by simpa using H) := by induction xs <;> simp_all

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