acc — Mathlib

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⟩

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