Mathlib Changelog
v4
Changelog
About
Github
Commit
2022-12-20 08:57
b78b790b
View on Github →
feat: port Order.CompleteBooleanAlgebra (
#1107
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Order/CompleteBooleanAlgebra.lean
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ₛ