Theorems · Inductive type · general topology

PseudoEpimorphism

(α : Type u_6) → (β : Type u_7) → [Preorder α] → [Preorder β] → Type (max u_6 u_7)

The type of pseudo-epimorphisms, aka p-morphisms, aka bounded maps, from α to β.

Defined in

Mathlib.Topology.Order.Hom.Esakia

Cited by

23 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

PreorderPreorder