map_pmap — Mathlib

English

If f₁ and f₂ are such that p(x) holds for all elements x of xs, then applying map with f₁ to pmap f₂ xs H is the same as pmap with f₁ ∘ f₂ on xs.

Русский

Если для всех элементов x в xs выполняется p(x), то отображение через f₁ после pmap f₂ xs H эквивалентно pmap с f₁ ∘ f₂ на xs.

LaTeX

$$$\text{map } f_1 (\text{pmap } f_2 xs H) = \text{pmap } (\lambda x hx. f_1 (f_2 x hx)) xs H$$$

Lean4

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

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