acc — Mathlib

English

If a is accessible under r whenever f a is accessible under s, then a is accessible under r.

Русский

Если из доступности $f(a)$ следует доступность $a$, то $a$ доступен по отношению $r$.

LaTeX

$$$\forall f\ a,\ Acc\ s (f\ a) \Rightarrow Acc\ r\ a$$$

Lean4

protected theorem acc [RelHomClass F r s] (f : F) (a : α) : Acc s (f a) → Acc r a :=
  by
  generalize h : f a = b
  intro ac
  induction ac generalizing a with
  | intro _ H IH => ?_
  subst h
  exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩

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