mathlib
4af7699b - feat(order/upper_lower): Maps of upper sets (#17007)

Commit

3 years ago

feat(order/upper_lower): Maps of upper sets (#17007) An order isomorphism of preorders induces an order isomorphisms of their upper sets.

Author

YaelDillies

Parents