Theorem LatticeCon.r_inf_sup_iff

Modification history

2025-09-19 18:56
Mathlib/Order/Lattice/Congruence.lean
feat(Order/Lattice): conditions for an equivalence relation to be a lattice congruence (#26836) …
Added LatticeCon.r_inf_sup_iffView on Github →