Theorems · Theorem · order theory

OrderIso.arrowCongr_apply

∀ {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] (f : α ≃o γ) (g : β ≃o δ) (p : α →o β),
  (f.arrowCongr g) p = (↑g).comp (p.comp ↑f.symm)

Defined in

Mathlib.Order.Hom.Basic

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

PreorderPreorderPreorderPreorder