Theorems · Theorem · logic and foundations

Acc.of_fibration

∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} (f : α → β),
  Relation.Fibration rα rβ f → ∀ {a : α}, Acc rα a → Acc rβ (f a)

If f : α → β is a fibration between relations rα and rβ, and a : α is accessible under rα, then f a is accessible under rβ.

Defined in

Mathlib.Logic.Relation

Cited by

4 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms