Theorems · Definition · order theory

ConditionallyCompletePartialOrder.mk.noConfusion

{α : Type u_3} →
  {P : Sort u} →
    {toConditionallyCompletePartialOrderSup : ConditionallyCompletePartialOrderSup α} →
      {toInfSet : InfSet α} →
        {isGLB_csInf_of_directed :
            ∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)} →
          {toConditionallyCompletePartialOrderSup' : ConditionallyCompletePartialOrderSup α} →
            {toInfSet' : InfSet α} →
              {isGLB_csInf_of_directed' :
                  ∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)} →
                { toConditionallyCompletePartialOrderSup := toConditionallyCompletePartialOrderSup,
                      toInfSet := toInfSet, isGLB_csInf_of_directed := isGLB_csInf_of_directed } =
                    { toConditionallyCompletePartialOrderSup := toConditionallyCompletePartialOrderSup',
                      toInfSet := toInfSet', isGLB_csInf_of_directed := isGLB_csInf_of_directed' } →
                  (toConditionallyCompletePartialOrderSup ≍ toConditionallyCompletePartialOrderSup' →
                      toInfSet ≍ toInfSet' → P) →
                    P

Defined in

Mathlib.Order.ConditionallyCompletePartialOrder.Defs

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms