mathlib3
c6ef6387 - feat(combinatorics/simple_graph/basic): Simple graphs form a complete boolean algebra (#18285)

Commit
2 years ago
feat(combinatorics/simple_graph/basic): Simple graphs form a complete boolean algebra (#18285) Upgrade the `boolean_algebra (simple_graph α)` and `lattice G.subgraph` instances to `complete_boolean_algebra (simple_graph α)` and `complete_distrib_lattice G.subgraph` respectively. Add `distrib_lattice`/`complete_distrib_lattice` instances for `G.finsubgraph`.
Author
Parents
Loading