Theorems · Inductive type · order theory

RelEmbedding

{α : Type u_5} → {β : Type u_6} → (α → α → Prop) → (β → β → Prop) → Type (max u_5 u_6)

A relation embedding with respect to a given pair of relations r and s is an embedding f : α ↪ β such that r a b ↔ s (f a) (f b).

Defined in

Mathlib.Order.RelIso.Basic

Cited by

281 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms