Theorems · Definition · order theory

CompleteLinearOrder.mk.noConfusion

{α : Type u_8} →
  {P : Sort u} →
    {toCompleteLattice : CompleteLattice α} →
      {toHImp : HImp α} →
        {le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c} →
          {toCompl : Compl α} →
            {himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ} →
              {toSDiff : SDiff α} →
                {sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c} →
                  {toHNot : HNot α} →
                    {top_sdiff : ∀ (a : α), ⊤ \ a = ￢a} →
                      {toOrd : Ord α} →
                        {le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a} →
                          {toDecidableLE : DecidableLE α} →
                            {toDecidableEq : DecidableEq α} →
                              {toDecidableLT : DecidableLT α} →
                                {compare_eq_compareOfLessAndEq :
                                    autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b)
                                      CompleteLinearOrder.compare_eq_compareOfLessAndEq._autoParam} →
                                  {toCompleteLattice' : CompleteLattice α} →
                                    {toHImp' : HImp α} →
                                      {le_himp_iff' : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c} →
                                        {toCompl' : Compl α} →
                                          {himp_bot' : ∀ (a : α), a ⇨ ⊥ = aᶜ} →
                                            {toSDiff' : SDiff α} →
                                              {sdiff_le_iff' : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c} →
                                                {toHNot' : HNot α} →
                                                  {top_sdiff' : ∀ (a : α), ⊤ \ a = ￢a} →
                                                    {toOrd' : Ord α} →
                                                      {le_total' : ∀ (a b : α), a ≤ b ∨ b ≤ a} →
                                                        {toDecidableLE' : DecidableLE α} →
                                                          {toDecidableEq' : DecidableEq α} →
                                                            {toDecidableLT' : DecidableLT α} →
                                                              {compare_eq_compareOfLessAndEq' :
                                                                  autoParam
                                                                    (∀ (a b : α), compare a b = compareOfLessAndEq a b)
                                                                    CompleteLinearOrder.compare_eq_compareOfLessAndEq._autoParam} →
                                                                { toCompleteLattice := toCompleteLattice,
                                                                      toHImp := toHImp, le_himp_iff := le_himp_iff,
                                                                      toCompl := toCompl, himp_bot := himp_bot,
                                                                      toSDiff := toSDiff, sdiff_le_iff := sdiff_le_iff,
                                                                      toHNot := toHNot, top_sdiff := top_sdiff,
                                                                      toOrd := toOrd, le_total := le_total,
                                                                      toDecidableLE := toDecidableLE,
                                                                      toDecidableEq := toDecidableEq,
                                                                      toDecidableLT := toDecidableLT,
                                                                      compare_eq_compareOfLessAndEq :=
                                                                        compare_eq_compareOfLessAndEq } =
                                                                    { toCompleteLattice := toCompleteLattice',
                                                                      toHImp := toHImp', le_himp_iff := le_himp_iff',
                                                                      toCompl := toCompl', himp_bot := himp_bot',
                                                                      toSDiff := toSDiff',
                                                                      sdiff_le_iff := sdiff_le_iff', toHNot := toHNot',
                                                                      top_sdiff := top_sdiff', toOrd := toOrd',
                                                                      le_total := le_total',
                                                                      toDecidableLE := toDecidableLE',
                                                                      toDecidableEq := toDecidableEq',
                                                                      toDecidableLT := toDecidableLT',
                                                                      compare_eq_compareOfLessAndEq :=
                                                                        compare_eq_compareOfLessAndEq' } →
                                                                  (toCompleteLattice ≍ toCompleteLattice' →
                                                                      toHImp ≍ toHImp' →
                                                                        toCompl ≍ toCompl' →
                                                                          toSDiff ≍ toSDiff' →
                                                                            toHNot ≍ toHNot' →
                                                                              toOrd ≍ toOrd' →
                                                                                toDecidableLE ≍ toDecidableLE' →
                                                                                  toDecidableEq ≍ toDecidableEq' →
                                                                                    toDecidableLT ≍ toDecidableLT' →
                                                                                      P) →
                                                                    P

Defined in

Mathlib.Order.CompleteLattice.Defs

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms