Theorems · Definition · order theory

RelHomClass.casesOn

{F : Type u_5} →
  {α : Type u_6} →
    {β : Type u_7} →
      {r : α → α → Prop} →
        {s : β → β → Prop} →
          [inst : FunLike F α β] →
            {motive : RelHomClass F r s → Sort u} →
              (t : RelHomClass F r s) → ((map_rel : ∀ (f : F) {a b : α}, r a b → s (f a) (f b)) → motive ⋯) → motive t

Defined in

Mathlib.Order.RelIso.Basic

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

FunLike