Theorems · Inductive type · order theory

CoheytingHom

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

The type of co-Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve difference.

Defined in

Mathlib.Order.Heyting.Hom

Cited by

20 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CoheytingAlgebraCoheytingAlgebra