Theorems · Theorem · order theory

RelHomClass.map_rel

∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {r : outParam (α → α → Prop)}
  {s : outParam (β → β → Prop)} {inst : FunLike F α β} [self : RelHomClass F r s] (f : F) {a b : α},
  r a b → s (f a) (f b)

A RelHomClass sends related elements to related elements

Defined in

Mathlib.Order.RelIso.Basic

Cited by

10 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

RelHomClass