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