English
Let p be a predicate on α, f a function α → β that assigns to each a a witness ha ∈ p(a). Then IsChain S (pmap f l hl) is equivalent to IsChain of the relation on l given by ∃ha ∃hb with S(f a ha, f b hb).
Русский
Пусть p — предикат на α, f : α → β с доказательствами ha ∈ p(a). Тогда IsChain S(pmap f l hl) эквивалентна IsChain по l для отношения, заданного через ∃ha ∃hb: S(f a ha, f b hb).
LaTeX
$$IsChain S (pmap f l hl) ↔ IsChain (\\lambda a b. ∃ ha ∃ hb, S (f a ha) (f b hb)) l$$
Lean4
theorem isChain_pmap {S : β → β → Prop} {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (hl : ∀ a ∈ l, p a) :
IsChain S (pmap f l hl) ↔ IsChain (fun a b => ∃ ha, ∃ hb, S (f a ha) (f b hb)) l := by
induction l using twoStepInduction <;> grind
