English
If f is a fibration between rα and rβ, accessibility is preserved along f.
Русский
Если f — фибрация между rα и rβ, то доступность по rβ сохраняется через f.
LaTeX
$$$\forall a:\alpha,\; Acc(r_β,f(a))$ given $Acc(r_α,a)$ and fib : Fibration(r_α,r_β,f)$$$
Lean4
/-- If `f : α → β` is a fibration between relations `rα` and `rβ`, and `a : α` is
accessible under `rα`, then `f a` is accessible under `rβ`. -/
theorem _root_.Acc.of_fibration (fib : Fibration rα rβ f) {a} (ha : Acc rα a) : Acc rβ (f a) :=
by
induction ha with
| intro a _ ih => ?_
refine Acc.intro (f a) fun b hr ↦ ?_
obtain ⟨a', hr', rfl⟩ := fib hr
exact ih a' hr'
