Commit 2023-08-08 18:01 cc20f815

View on Github →

feat(GaloisConnection): add 2 lemmas (#6441)

Estimated changes

Modified Mathlib/Order/GaloisConnection.lean

added theorem GaloisCoinsertion.u_bot

added theorem GaloisInsertion.l_top