mathlib
c64b2b4b - feat(order/upper_lower): Upper sets correspond to monotone predicates (#17241)

Commit

3 years ago

feat(order/upper_lower): Upper sets correspond to monotone predicates (#17241) `is_upper_set {a | p a} ↔ monotone p` and similar.

Author

YaelDillies

Parents