Theorem GaloisConnection.exists_eq_l

Modification history

2026-02-05 04:02
Mathlib/Order/GaloisConnection/Defs.lean
feat(to_dual): use the new `to_dual_cast` framework (#34042) …
Deleted GaloisConnection.exists_eq_lView on Github →
2025-01-20 11:09
Mathlib/Order/GaloisConnection/Basic.lean
chore(Order): split `GaloisConnection` into `Defs.lean` and `Basic.lean` (#20798) …
Modified GaloisConnection.exists_eq_lView on Github →
2024-01-16 22:20
Mathlib/Order/GaloisConnection.lean
chore(GaloisConnection): golf using `dual` (#9786)
Modified GaloisConnection.exists_eq_lView on Github →
2022-12-19 23:59
Mathlib/Order/GaloisConnection.lean
feat: port Order.GaloisConnection (#1099)
Added GaloisConnection.exists_eq_lView on Github →