Theorem GaloisInsertion.l_top

Modification history

2025-01-20 11:09

Mathlib/Order/GaloisConnection/Basic.lean

chore(Order): split `GaloisConnection` into `Defs.lean` and `Basic.lean` (#20798) …

Modified GaloisInsertion.l_top View on Github →

2023-08-08 18:01

Mathlib/Order/GaloisConnection.lean

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

Added GaloisInsertion.l_top View on Github →