Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-02-25 04:10
caed8413
View on Github →
feat(order/complete_lattice): add complete_lattice.independent.disjoint{_Sup,} (
#6405
)
Estimated changes
Modified
src/order/compactly_generated.lean
Modified
src/order/complete_lattice.lean
added
theorem
Inf_sup_le_infi_sup
added
theorem
complete_lattice.independent.disjoint
added
theorem
complete_lattice.independent.disjoint_Sup
modified
theorem
complete_lattice.independent.mono
modified
def
complete_lattice.independent
modified
theorem
complete_lattice.independent_empty
added
theorem
disjoint_Sup_left
added
theorem
disjoint_Sup_right
added
theorem
supr_inf_le_Sup_inf
Modified
src/order/omega_complete_partial_order.lean