Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-05-07 09:30
11a06de1
View on Github →
feat(order/closure): closure of unions and bUnions (
#7361
) prove closure_closure_union and similar
Estimated changes
Modified
src/order/closure.lean
added
theorem
closure_operator.closure_bsupr_closure
added
theorem
closure_operator.closure_inf_le
deleted
theorem
closure_operator.closure_inter_le
modified
theorem
closure_operator.closure_le_closed_iff_le
added
theorem
closure_operator.closure_le_mk₃_iff
added
theorem
closure_operator.closure_mem_mk₃
added
theorem
closure_operator.closure_sup_closure
added
theorem
closure_operator.closure_sup_closure_le
added
theorem
closure_operator.closure_sup_closure_left
added
theorem
closure_operator.closure_sup_closure_right
added
theorem
closure_operator.closure_supr_closure
modified
theorem
closure_operator.closure_top
deleted
theorem
closure_operator.closure_union_closure_le
added
theorem
closure_operator.eq_mk₃_closed
added
theorem
closure_operator.mem_mk₃_closed
added
def
closure_operator.mk₂
added
def
closure_operator.mk₃
Modified
src/order/complete_lattice.lean
added
theorem
Sup_le_Sup_of_subset_insert_bot
deleted
theorem
Sup_le_Sup_of_subset_instert_bot