Commit 2022-12-20 08:57 b78b790b

View on Github →

feat: port Order.CompleteBooleanAlgebra (#1107)

Estimated changes

added theorem PUnit.infₛ_eq
added theorem PUnit.supₛ_eq
added theorem binfᵢ_sup_binfᵢ
added theorem bsupᵢ_inf_bsupᵢ
added theorem compl_infᵢ
added theorem compl_infₛ'
added theorem compl_infₛ
added theorem compl_supᵢ
added theorem compl_supₛ'
added theorem compl_supₛ
added theorem disjoint_supᵢ_iff
added theorem disjoint_supᵢ₂_iff
added theorem disjoint_supₛ_iff
added theorem inf_supᵢ_eq
added theorem inf_supᵢ₂_eq
added theorem inf_supₛ_eq
added theorem infᵢ_sup_eq
added theorem infᵢ_sup_infᵢ
added theorem infᵢ_sup_of_antitone
added theorem infᵢ_sup_of_monotone
added theorem infᵢ₂_sup_eq
added theorem infₛ_sup_eq
added theorem infₛ_sup_infₛ
added theorem sup_infᵢ_eq
added theorem sup_infᵢ₂_eq
added theorem sup_infₛ_eq
added theorem supᵢ_disjoint_iff
added theorem supᵢ_inf_eq
added theorem supᵢ_inf_of_antitone
added theorem supᵢ_inf_of_monotone
added theorem supᵢ_inf_supᵢ
added theorem supᵢ₂_disjoint_iff
added theorem supᵢ₂_inf_eq
added theorem supₛ_disjoint_iff
added theorem supₛ_inf_eq
added theorem supₛ_inf_supₛ