Theorems · Definition · logic and foundations

Relation.Fibration

{α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → (α → β) → Prop

A function f : α → β is a fibration between the relation rα and rβ if for all a : α and b : β, whenever b : β and f a are related by rβ, b is the image of some a' : α under f, and a' and a are related by rα.

Defined in

Mathlib.Logic.Relation

Cited by

14 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms