English
Let p be a predicate on β and f : β → α with hl specifying which elements satisfy p. Then IsChain R (f a ha :: pmap f l hl) is equivalent to IsChain on a :: l with the corresponding existential relation.
Русский
Пусть p — предикат на β и f : β → α, тогда IsChain R (f a ha :: pmap f l hl) эквивалентна IsChain на a :: l с соответствующим существовательным отношением.
LaTeX
$$IsChain R (f a ha :: pmap f l hl) ↔ IsChain (\\lambda a b. ∃ ha ∃ hb, R (f a ha) (f b hb)) (a :: l)$$
Lean4
theorem isChain_cons_pmap {p : β → Prop} (f : ∀ b, p b → α) {l : List β} (hl : ∀ b ∈ l, p b) {a} (ha) :
IsChain R (f a ha :: pmap f l hl) ↔ IsChain (fun a b => ∃ ha, ∃ hb, R (f a ha) (f b hb)) (a :: l) :=
isChain_pmap (l := a :: _) f (by grind)
