English
For any f : InitialSeg r s and a ∈ α, Acc r a iff Acc s (f a).
Русский
Для f : InitialSeg r s и a, Acc r a эквивалентно Acc s (f a).
LaTeX
$$$Acc\\,r\\ a \\leftrightarrow Acc\\,s\\,(f\\,a).$$$
Lean4
protected theorem acc (f : r ≼i s) (a : α) : Acc r a ↔ Acc s (f a) :=
⟨by
refine fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => ?_
obtain ⟨a', rfl⟩ := f.mem_range_of_rel hb
exact ha _ (f.map_rel_iff.mp hb), f.toRelEmbedding.acc a⟩