Commit 2023-04-20 11:28 5a5f6d5a

View on Github →

chore: forward port leanprover-community/mathlib#18442 (#3545)

leanprover-community/mathlib#18442

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj

added theorem SimpleGraph.ConnectedComponent.connectedComponentMk_mem

added def SimpleGraph.ConnectedComponent.isoEquivSupp

added theorem SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp

added theorem SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map

added theorem SimpleGraph.ConnectedComponent.mem_supp_iff

added def SimpleGraph.ConnectedComponent.supp

added theorem SimpleGraph.ConnectedComponent.supp_inj

added theorem SimpleGraph.ConnectedComponent.supp_injective

added def SimpleGraph.Iso.connectedComponentEquiv

added theorem SimpleGraph.Iso.connectedComponentEquiv_refl

added theorem SimpleGraph.Iso.connectedComponentEquiv_symm

added theorem SimpleGraph.Iso.connectedComponentEquiv_trans

added theorem SimpleGraph.Iso.reachable_iff

added theorem SimpleGraph.Iso.symm_apply_reachable