Theorems · Definition · order theory

OmegaCompletePartialOrder.Chain.map

{α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → OmegaCompletePartialOrder.Chain α → (α →o β) → OmegaCompletePartialOrder.Chain β

map function for Chain

Defined in

Mathlib.Order.OmegaCompletePartialOrder

Cited by

41 results in Mathlib

Foundations

Depth 22 from the axioms · uses no axioms

Assumes

PreorderPreorder