Commit 2024-10-02 17:17 24484cb7

View on Github →

feat(Subgraph): API lemmas (#17332) From LeanCamCombi

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.IsInduced.top

added theorem SimpleGraph.Subgraph.coe_bot

added theorem SimpleGraph.Subgraph.edgeSet_coe

added theorem SimpleGraph.Subgraph.image_coe_edgeSet_coe

added theorem SimpleGraph.Subgraph.map_comp

added theorem SimpleGraph.Subgraph.map_id

added theorem SimpleGraph.Subgraph.map_mono

modified theorem SimpleGraph.Subgraph.map_monotone

modified theorem SimpleGraph.Subgraph.map_sup

deleted theorem SimpleGraph.Subgraph.mem_edgeSet

deleted theorem SimpleGraph.Subgraph.mem_verts_if_mem_edge

added theorem SimpleGraph.Subgraph.mem_verts_of_mem_edge

added theorem SimpleGraph.Subgraph.spanningCoe_le

added def SimpleGraph.Subgraph.topIso