Theorems · Theorem · order theory

Nucleus.mk.inj

∀ {X : Type u_2} {inst : SemilatticeInf 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_1 : InfHom X X}
  {idempotent'_1 : ∀ (x : X), toInfHom_1.toFun (toInfHom_1.toFun x) ≤ toInfHom_1.toFun x}
  {le_apply'_1 : ∀ (x : X), x ≤ toInfHom_1.toFun x},
  { toInfHom := toInfHom, idempotent' := idempotent', le_apply' := le_apply' } =
      { toInfHom := toInfHom_1, idempotent' := idempotent'_1, le_apply' := le_apply'_1 } →
    toInfHom = toInfHom_1

Defined in

Mathlib.Order.Nucleus

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms