Theorems · Theorem · order theory

ClosureOperator.mk.inj

∀ {α : Type u_1} {inst : Preorder α} {toOrderHom : α →o α} {le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x}
  {idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x} {IsClosed : α → Prop}
  {isClosed_iff : autoParam (∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x) ClosureOperator.isClosed_iff._autoParam}
  {toOrderHom_1 : α →o α} {le_closure'_1 : ∀ (x : α), x ≤ toOrderHom_1.toFun x}
  {idempotent'_1 : ∀ (x : α), toOrderHom_1.toFun (toOrderHom_1.toFun x) = toOrderHom_1.toFun x} {IsClosed_1 : α → Prop}
  {isClosed_iff_1 :
    autoParam (∀ {x : α}, IsClosed_1 x ↔ toOrderHom_1.toFun x = x) ClosureOperator.isClosed_iff._autoParam},
  { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
        isClosed_iff := isClosed_iff } =
      { toOrderHom := toOrderHom_1, le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
        isClosed_iff := isClosed_iff_1 } →
    toOrderHom = toOrderHom_1 ∧ IsClosed = IsClosed_1

Defined in

Mathlib.Order.Closure

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms