pmap_map — Mathlib

English

Mapping after pmap equals pmap after mapping: (z.pmap f h).map g = z.pmap (a ↦ g (f a (h a a_h))) (λ _ a_h, a_h).

Русский

Отображение после pmap равно pmap после отображения: (z.pmap f h).map g = z.pmap (λ a ha, g (f a (h a ha))) (λ _ ha, ha).

LaTeX

$$$ (z.pmap f h).map g = z.pmap (\\lambda a ha => g (f a (h a ha))) (\\lambda _ ha => ha). $$$

Lean4

theorem pmap_map {P : α → Prop} {Q : β → Prop} (f : ∀ a, P a → β) (g : β → γ) (z : Sym2 α) (h : ∀ a ∈ z, P a)
    (h' : ∀ b ∈ z.pmap f h, Q b) : (z.pmap f h).map g = z.pmap (fun a ha => g (f a (h a ha))) (fun _ ha ↦ ha) := by
  cases z; rfl

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