Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-23 01:31 ab6bcd63

View on Github →

feat(order/upper_lower): Upper closure of a set (#15581) Define the upper/lower set generated by a set.

Estimated changes

added theorem coe_lower_closure
added theorem coe_upper_closure
added theorem gc_lower_closure_coe
added theorem gc_upper_closure_coe
added def lower_closure
added theorem lower_closure_Union
added theorem lower_closure_empty
added theorem lower_closure_min
added theorem lower_closure_mono
added theorem lower_closure_sUnion
added theorem lower_closure_union
added theorem lower_closure_univ
modified theorem lower_set.coe_Inf
modified theorem lower_set.coe_Sup
modified theorem lower_set.coe_bot
modified theorem lower_set.coe_inf
modified theorem lower_set.coe_infi
modified theorem lower_set.coe_infi₂
modified theorem lower_set.coe_sup
modified theorem lower_set.coe_supr
modified theorem lower_set.coe_supr₂
modified theorem lower_set.coe_top
added theorem lower_set.supr_Iic
added theorem mem_lower_closure
added theorem mem_upper_closure
added theorem subset_lower_closure
added theorem subset_upper_closure
added def upper_closure
added theorem upper_closure_Union
added theorem upper_closure_anti
added theorem upper_closure_empty
added theorem upper_closure_min
added theorem upper_closure_sUnion
added theorem upper_closure_union
added theorem upper_closure_univ
modified theorem upper_set.coe_Inf
modified theorem upper_set.coe_Sup
modified theorem upper_set.coe_bot
modified theorem upper_set.coe_inf
modified theorem upper_set.coe_infi
modified theorem upper_set.coe_infi₂
modified theorem upper_set.coe_sup
modified theorem upper_set.coe_supr
modified theorem upper_set.coe_supr₂
modified theorem upper_set.coe_top
added theorem upper_set.infi_Ici