Commit 2025-05-24 12:26 2d8a905c

View on Github →

feat: relative upper/lower sets (#23762) From a comment by @b-mehta on Zulip in response to me formalising IMO 2015 Q6 (#23038).

Estimated changes

added def IsRelLowerSet
added def IsRelUpperSet
added structure RelLowerSet
added structure RelUpperSet
added theorem IsRelLowerSet.inter
added theorem IsRelLowerSet.union
added theorem IsRelUpperSet.inter
added theorem IsRelUpperSet.union
added theorem isRelLowerSet_Icc_ge
added theorem isRelLowerSet_empty
added theorem isRelLowerSet_self
added theorem isRelUpperSet_Icc_le
added theorem isRelUpperSet_empty
added theorem isRelUpperSet_self