Theorems · Definition · general topology

EsakiaHom.toContinuousOrderHom

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

Defined in

Mathlib.Topology.Order.Hom.Esakia

Cited by

3 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpacePreorderTopologicalSpacePreorder