Theorems · Definition · general topology

ContinuousOrderHom.toOrderHom

{α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : TopologicalSpace α] → [inst_3 : TopologicalSpace β] → (α →Co β) → α →o β

Defined in

Mathlib.Topology.Order.Hom.Basic

Cited by

8 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

PreorderPreorderTopologicalSpaceTopologicalSpace