Theorems · Definition · order theory

OrderIso.arrowCongr

{α : Type u_6} →
  {β : Type u_7} →
    {γ : Type u_8} →
      {δ : Type u_9} →
        [inst : Preorder α] →
          [inst_1 : Preorder β] → [inst_2 : Preorder γ] → [inst_3 : Preorder δ] → α ≃o γ → β ≃o δ → (α →o β) ≃o (γ →o δ)

An order isomorphism between the domains and codomains of two prosets of order homomorphisms gives an order isomorphism between the two function prosets.

Defined in

Mathlib.Order.Hom.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

PreorderPreorderPreorderPreorder