Commit 2026-04-03 20:46 d467a9fa

View on Github →

feat(Combinatorics/SimpleGraph/Maps): lemmas about support (#35615)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.Adj.left_mem_support

added theorem SimpleGraph.Adj.right_mem_support

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.induce_bot

added theorem SimpleGraph.spanningCoe_induce_eq_self

added theorem SimpleGraph.spanningCoe_induce_support

added theorem SimpleGraph.spanningCoe_induce_univ

added theorem SimpleGraph.support_comap_subset

added theorem SimpleGraph.support_induce_subset_coe_preimage

added theorem SimpleGraph.support_induce_subset_coe_preimage_support

added theorem SimpleGraph.support_spanningCoe