mathlib3
4a59a4d4 - chore(order/galois_connection): Make lifting instances reducible (#12559)

Commit

3 years ago

chore(order/galois_connection): Make lifting instances reducible (#12559) and provide `infi₂` and `supr₂` versions of the lemmas.

Author

YaelDillies

Parents