Commit 2023-05-16 13:10 5680c5a3

View on Github →

feat: port Combinatorics.SimpleGraph.Ends.Defs (#4002)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

added theorem SimpleGraph.ComponentCompl.coe_inj

added theorem SimpleGraph.ComponentCompl.exists_adj_boundary_pair

added def SimpleGraph.ComponentCompl.hom

added theorem SimpleGraph.ComponentCompl.hom_eq_iff_le

added theorem SimpleGraph.ComponentCompl.hom_eq_iff_not_disjoint

added theorem SimpleGraph.ComponentCompl.hom_infinite

added theorem SimpleGraph.ComponentCompl.hom_mk

added theorem SimpleGraph.ComponentCompl.hom_refl

added theorem SimpleGraph.ComponentCompl.hom_trans

added theorem SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges

added theorem SimpleGraph.ComponentCompl.mem_of_adj

added theorem SimpleGraph.ComponentCompl.mem_supp_iff

added theorem SimpleGraph.ComponentCompl.not_mem_of_mem

added theorem SimpleGraph.ComponentCompl.subset_hom

added def SimpleGraph.ComponentCompl.supp

added theorem SimpleGraph.ComponentCompl.supp_inj

added theorem SimpleGraph.ComponentCompl.supp_injective

added def SimpleGraph.ComponentCompl

added def SimpleGraph.componentComplFunctor

added def SimpleGraph.componentComplMk

added theorem SimpleGraph.componentComplMk_eq_of_adj

added theorem SimpleGraph.componentComplMk_mem

added theorem SimpleGraph.componentComplMk_mem_hom

added theorem SimpleGraph.end_hom_mk_of_mk

added theorem SimpleGraph.infinite_iff_in_eventualRange