Theorems · Definition · order theory

FrameHom.noConfusionType

Sort u →
  {α : Type u_8} →
    {β : Type u_9} →
      [inst : CompleteLattice α] →
        [inst_1 : CompleteLattice β] →
          FrameHom α β →
            {α' : Type u_8} →
              {β' : Type u_9} → [inst' : CompleteLattice α'] → [inst'_1 : CompleteLattice β'] → FrameHom α' β' → Sort u

Defined in

Mathlib.Order.Hom.CompleteLattice

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

CompleteLatticeCompleteLatticeCompleteLatticeCompleteLattice