mathlib

f5170fc5 - feat(order/bounded_order): Codisjointness (#14195)

feat(order/bounded_order): Codisjointness (#14195) Define `codisjoint`, the dual notion of `disjoint`. This is already used without a name in `is_compl`, and will soon be used for Heyting algebras.