Commit 2023-10-21 10:50 512169bb

View on Github →

feat: Removing elements from a lower set (#7374) If a set t is an upper set inside a lower set s, then s \ t is a lower set.

Estimated changes

added theorem SetLike.coe_ne_coe
added theorem IsLowerSet.erase
added theorem IsLowerSet.sdiff
added theorem IsUpperSet.erase
added theorem IsUpperSet.sdiff
added theorem LowerSet.Iic_inj
added theorem LowerSet.Iic_le
added theorem LowerSet.Iic_ne_Iic
added theorem LowerSet.Iic_ne_bot
added theorem LowerSet.Iic_sup_erase
added theorem LowerSet.bot_lt_Iic
added theorem LowerSet.coe_erase
added theorem LowerSet.coe_mk
added theorem LowerSet.coe_nonempty
added theorem LowerSet.coe_sdiff
modified theorem LowerSet.coe_subset_coe
added def LowerSet.erase
added theorem LowerSet.erase_eq
added theorem LowerSet.erase_idem
added theorem LowerSet.erase_le
added theorem LowerSet.erase_lt
added theorem LowerSet.erase_sup_Iic
modified theorem LowerSet.mem_mk
added def LowerSet.sdiff
added theorem LowerSet.sdiff_le_left
added theorem LowerSet.sdiff_lt_left
added theorem UpperSet.Ici_inf_erase
added theorem UpperSet.Ici_inj
added theorem UpperSet.Ici_lt_top
added theorem UpperSet.Ici_ne_Ici
added theorem UpperSet.Ici_ne_top
added theorem UpperSet.coe_erase
added theorem UpperSet.coe_mk
added theorem UpperSet.coe_nonempty
added theorem UpperSet.coe_sdiff
added def UpperSet.erase
added theorem UpperSet.erase_eq
added theorem UpperSet.erase_idem
added theorem UpperSet.erase_inf_Ici
added theorem UpperSet.le_Ici
added theorem UpperSet.le_erase
added theorem UpperSet.le_sdiff_left
added theorem UpperSet.lt_erase
added theorem UpperSet.lt_sdiff_left
modified theorem UpperSet.mem_mk
added def UpperSet.sdiff
added theorem le_upperClosure
added theorem lowerClosure_le