Commit 2024-02-11 19:22 d18f1d0b

View on Github →

chore(Order/*): move SupSet, Set.sUnion etc to a new file (#10232)

Estimated changes

deleted theorem Set.iInf_eq_iInter
deleted def Set.iInter
deleted theorem Set.iSup_eq_iUnion
deleted def Set.iUnion
deleted def Set.iUnion_delab
deleted theorem Set.mem_iInter
deleted theorem Set.mem_iUnion
deleted theorem Set.mem_sInter
deleted theorem Set.mem_sUnion
deleted theorem Set.sInf_eq_sInter
deleted def Set.sInter
deleted def Set.sInter_delab
deleted theorem Set.sSup_eq_sUnion
deleted def Set.sUnion
deleted def iInf
deleted def iInf_delab
deleted def iSup
deleted def iSup_delab
added theorem Set.iInf_eq_iInter
added def Set.iInter
added theorem Set.iSup_eq_iUnion
added def Set.iUnion
added def Set.iUnion_delab
added theorem Set.mem_iInter
added theorem Set.mem_iUnion
added theorem Set.mem_sInter
added theorem Set.mem_sUnion
added theorem Set.sInf_eq_sInter
added def Set.sInter
added def Set.sInter_delab
added theorem Set.sSup_eq_sUnion
added def Set.sUnion
added def iInf
added def iInf_delab
added def iSup
added def iSup_delab