Theorems · Inductive type · order theory

RelHomClass

(F : Type u_5) →
  {α : outParam (Type u_6)} →
    {β : outParam (Type u_7)} → outParam (α → α → Prop) → outParam (β → β → Prop) → [FunLike F α β] → Prop

RelHomClass F r s asserts that F is a type of functions such that all f : F satisfy r a b → s (f a) (f b). The relations r and s are outParams since figuring them out from a goal is a higher-order matching problem that Lean usually can't do unaided.

Defined in

Mathlib.Order.RelIso.Basic

Cited by

13 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

FunLike