Theorems · Definition · order theory

RelIso.toRelEmbedding

{α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → r ↪r s

Convert a RelIso to a RelEmbedding. This function is also available as a coercion but often it is easier to write f.toRelEmbedding than to write explicitly r and s in the target type.

Defined in

Mathlib.Order.RelIso.Basic

Cited by

34 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound