English
Composing two pmaps is the same as a single pmap with the composed data: (z.pmap f z h).pmap g h' = z.pmap (λ a ha => g (f a (h a ha)) (h' _ ((mem_pmap_iff f z h _).mpr ⟨a, ha, rfl⟩))) (λ _ ha, ha).
Русский
Композиция двух pmap равна одному pmap с композиционными данными.
LaTeX
$$$ (z.pmap f z h).pmap g h' = z.pmap (\\lambda a ha => g (f a (h a ha)) (h' _ ((mem_pmap_iff f z h _).mpr \\langle a, ha, rfl \\rangle))) (\\lambda _ ha, ha). $$$
Lean4
theorem pmap_pmap {P : α → Prop} {Q : β → Prop} (f : ∀ a, P a → β) (g : ∀ b, Q b → γ) (z : Sym2 α) (h : ∀ a ∈ z, P a)
(h' : ∀ b ∈ z.pmap f h, Q b) :
(z.pmap f h).pmap g h' =
z.pmap (fun a ha => g (f a (h a ha)) (h' _ ((mem_pmap_iff f z h _).mpr ⟨a, ha, rfl⟩))) (fun _ ha ↦ ha) :=
by cases z; rfl
