Theorems · Definition · order theory

CompleteAtomicBooleanAlgebra.mk.noConfusion

{α : Type u} →
  {P : Sort u_1} →
    {toCompleteBooleanAlgebra : CompleteBooleanAlgebra α} →
      {iInf_iSup_eq : ∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)} →
        {toCompleteBooleanAlgebra' : CompleteBooleanAlgebra α} →
          {iInf_iSup_eq' :
              ∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)} →
            { toCompleteBooleanAlgebra := toCompleteBooleanAlgebra, iInf_iSup_eq := iInf_iSup_eq } =
                { toCompleteBooleanAlgebra := toCompleteBooleanAlgebra', iInf_iSup_eq := iInf_iSup_eq' } →
              (toCompleteBooleanAlgebra ≍ toCompleteBooleanAlgebra' → P) → P

Defined in

Mathlib.Order.CompleteBooleanAlgebra

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms