Theorems · Definition · order theory

ClosureOperator.mk.noConfusion

{α : Type u_1} →
  {inst : Preorder α} →
    {P : Sort u} →
      {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' : α →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 := toOrderHom, le_closure' := le_closure', idempotent' := idempotent',
                                IsClosed := IsClosed, isClosed_iff := isClosed_iff } =
                              { toOrderHom := toOrderHom', le_closure' := le_closure'', idempotent' := idempotent'',
                                IsClosed := IsClosed', isClosed_iff := isClosed_iff' } →
                            (toOrderHom ≍ toOrderHom' → IsClosed ≍ IsClosed' → P) → P

Defined in

Mathlib.Order.Closure

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms