Theorems · Definition · order theory

CompleteLatticeHom.mk.noConfusion

{α : Type u_8} →
  {β : Type u_9} →
    {inst : CompleteLattice α} →
      {inst_1 : CompleteLattice β} →
        {P : Sort u} →
          {tosInfHom : sInfHom α β} →
            {map_sSup' : ∀ (s : Set α), tosInfHom.toFun (sSup s) = sSup (tosInfHom.toFun '' s)} →
              {tosInfHom' : sInfHom α β} →
                {map_sSup'' : ∀ (s : Set α), tosInfHom'.toFun (sSup s) = sSup (tosInfHom'.toFun '' s)} →
                  { tosInfHom := tosInfHom, map_sSup' := map_sSup' } =
                      { tosInfHom := tosInfHom', map_sSup' := map_sSup'' } →
                    (tosInfHom ≍ tosInfHom' → P) → P

Defined in

Mathlib.Order.Hom.CompleteLattice

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms