Theorems · Definition · order theory

FrameHom.noConfusion

{P : Sort u} →
  {α : Type u_8} →
    {β : Type u_9} →
      {inst : CompleteLattice α} →
        {inst_1 : CompleteLattice β} →
          {t : FrameHom α β} →
            {α' : Type u_8} →
              {β' : Type u_9} →
                {inst' : CompleteLattice α'} →
                  {inst'_1 : CompleteLattice β'} →
                    {t' : FrameHom α' β'} →
                      α = α' → β = β' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → FrameHom.noConfusionType P t t'

Defined in

Mathlib.Order.Hom.CompleteLattice

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms