Theorems · Definition · order theory

RelEmbedding.ofMapRelIff

{α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} → (f : α → β) → [Std.Antisymm r] → [Std.Refl s] → (∀ (a b : α), s (f a) (f b) ↔ r a b) → r ↪r s

To define a relation embedding from an antisymmetric relation r to a reflexive relation s it suffices to give a function together with a proof that it satisfies s (f a) (f b) ↔ r a b.

Defined in

Mathlib.Order.RelIso.Basic

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

Std.AntisymmStd.Refl