Commit 2023-03-27 21:01 f7b1c219

View on Github →

feat: Simple graphs form a complete boolean algebra (#2502) Match https://github.com/leanprover-community/mathlib/pull/18285

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.adj_inj

added theorem SimpleGraph.adj_injective

added theorem SimpleGraph.infᵢ_adj

added theorem SimpleGraph.infᵢ_adj_of_nonempty

added theorem SimpleGraph.infₛ_adj

added theorem SimpleGraph.infₛ_adj_of_nonempty

added theorem SimpleGraph.supᵢ_adj

added theorem SimpleGraph.supₛ_adj

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

deleted def SimpleGraph.Subgraph.IsSubgraph

deleted def SimpleGraph.Subgraph.bot

deleted theorem SimpleGraph.Subgraph.bot_verts

added theorem SimpleGraph.Subgraph.edgeSet_infᵢ

added theorem SimpleGraph.Subgraph.edgeSet_infₛ

added theorem SimpleGraph.Subgraph.edgeSet_supᵢ

added theorem SimpleGraph.Subgraph.edgeSet_supₛ

modified theorem SimpleGraph.Subgraph.inf_adj

added theorem SimpleGraph.Subgraph.infᵢ_adj

added theorem SimpleGraph.Subgraph.infᵢ_adj_of_nonempty

added theorem SimpleGraph.Subgraph.infₛ_adj

added theorem SimpleGraph.Subgraph.infₛ_adj_of_nonempty

deleted def SimpleGraph.Subgraph.inter

added theorem SimpleGraph.Subgraph.neighborSet_bot

added theorem SimpleGraph.Subgraph.neighborSet_infᵢ

added theorem SimpleGraph.Subgraph.neighborSet_infₛ

added theorem SimpleGraph.Subgraph.neighborSet_supᵢ

added theorem SimpleGraph.Subgraph.neighborSet_supₛ

added theorem SimpleGraph.Subgraph.neighborSet_top

modified theorem SimpleGraph.Subgraph.not_bot_adj

added theorem SimpleGraph.Subgraph.spanningCoe_inj

modified theorem SimpleGraph.Subgraph.sup_adj

added theorem SimpleGraph.Subgraph.supᵢ_adj

added theorem SimpleGraph.Subgraph.supₛ_adj

deleted def SimpleGraph.Subgraph.top

added theorem SimpleGraph.Subgraph.top_adj

deleted theorem SimpleGraph.Subgraph.top_adj_iff

deleted theorem SimpleGraph.Subgraph.top_verts

deleted def SimpleGraph.Subgraph.union

added theorem SimpleGraph.Subgraph.verts_bot

modified theorem SimpleGraph.Subgraph.verts_inf

added theorem SimpleGraph.Subgraph.verts_infᵢ

added theorem SimpleGraph.Subgraph.verts_infₛ

modified theorem SimpleGraph.Subgraph.verts_sup

added theorem SimpleGraph.Subgraph.verts_supᵢ

added theorem SimpleGraph.Subgraph.verts_supₛ

added theorem SimpleGraph.Subgraph.verts_top