Theorems · Definition · order theory

Nucleus.mk.noConfusion

{X : Type u_2} →
  {inst : SemilatticeInf X} →
    {P : Sort u} →
      {toInfHom : InfHom X X} →
        {idempotent' : ∀ (x : X), toInfHom.toFun (toInfHom.toFun x) ≤ toInfHom.toFun x} →
          {le_apply' : ∀ (x : X), x ≤ toInfHom.toFun x} →
            {toInfHom' : InfHom X X} →
              {idempotent'' : ∀ (x : X), toInfHom'.toFun (toInfHom'.toFun x) ≤ toInfHom'.toFun x} →
                {le_apply'' : ∀ (x : X), x ≤ toInfHom'.toFun x} →
                  { toInfHom := toInfHom, idempotent' := idempotent', le_apply' := le_apply' } =
                      { toInfHom := toInfHom', idempotent' := idempotent'', le_apply' := le_apply'' } →
                    (toInfHom ≍ toInfHom' → P) → P

Defined in

Mathlib.Order.Nucleus

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms