Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-08 18:27 db53863f

View on Github →

feat(combinatorics/simple_graph/ends): Definition (only) of the ends of a simple_graph. (#17857)

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.coe_induce_hom

added def simple_graph.induce_hom

added theorem simple_graph.induce_hom_comp

added theorem simple_graph.induce_hom_id

Modified src/combinatorics/simple_graph/connectivity.lean

added def simple_graph.connected_component.map

added theorem simple_graph.connected_component.map_comp

added theorem simple_graph.connected_component.map_id

added theorem simple_graph.connected_component.map_mk

added theorem simple_graph.walk.exists_boundary_dart

Created src/combinatorics/simple_graph/ends/defs.lean

added theorem simple_graph.component_compl.coe_inj

added theorem simple_graph.component_compl.exists_adj_boundary_pair

added def simple_graph.component_compl.hom

added theorem simple_graph.component_compl.hom_eq_iff_le

added theorem simple_graph.component_compl.hom_eq_iff_not_disjoint

added theorem simple_graph.component_compl.hom_infinite

added theorem simple_graph.component_compl.hom_mk

added theorem simple_graph.component_compl.hom_refl

added theorem simple_graph.component_compl.hom_trans

added theorem simple_graph.component_compl.infinite_iff_in_all_ranges

added theorem simple_graph.component_compl.mem_of_adj

added theorem simple_graph.component_compl.mem_supp_iff

added theorem simple_graph.component_compl.not_mem_of_mem

added theorem simple_graph.component_compl.subset_hom

added def simple_graph.component_compl.supp

added theorem simple_graph.component_compl.supp_inj

added theorem simple_graph.component_compl.supp_injective

added def simple_graph.component_compl

added def simple_graph.component_compl_functor

added def simple_graph.component_compl_mk

added theorem simple_graph.component_compl_mk_eq_of_adj

added theorem simple_graph.component_compl_mk_mem

added theorem simple_graph.component_compl_mk_mem_hom

added theorem simple_graph.end_hom_mk_of_mk

added theorem simple_graph.infinite_iff_in_eventual_range

added def simple_graph.«end»

Created src/combinatorics/simple_graph/ends/properties.lean