Commit 2026-01-13 16:45 3533acd2

View on Github →

feat(GraphTheory): supports of top and bot graphs (#33856)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.support_bot

added theorem SimpleGraph.support_eq_bot_iff

added theorem SimpleGraph.support_of_subsingleton

added theorem SimpleGraph.support_top_of_nontrivial

Modified Mathlib/Data/Rel.lean

added theorem SetRel.cod_eq_empty_iff

added theorem SetRel.dom_eq_empty_iff