Commit 2025-08-24 22:56 b3a7cef5
View on Github →feat(Combinatorics/SimpleGraph): relate ⊤ ⊑ · to the existence of a clique (#28785)
Proves that the image/map of a Copy ⊤ · is a clique and that a simple graph is clique-free iff it does not contain ⊤.