Sym2

📁 Source: Mathlib/Data/Sym/Sym2.lean

Statistics

Metric	Count
Definitions sym2Map, sym2, Sym2, decidablePred, decidable, other, other', setoid, ToRel, add, attachWith, decidablePred_mem_diagSet, diag, diagSet, equivMultiset, equivSym, fromRel, decidablePred, fromRelOrderEmbedding, hrec, instDecidableEq, instDecidableRel, instDecidableRel', instPartialOrder, instRepr, instSetLike, instUnique, lift₂, map, mk, mkEmbedding, mul, pmap, rec, recOn, recOnSubsingleton, sym2EquivSym', toFinset, toMultiset, «termS(_,_)»»)	40
Theorems sym2Map_apply, mem_sym2_iff_subset, mk'_mem_sym2_iff, mk_mem_sym2_iff, mk_preimage_sym2, sym2_empty, sym2_eq_mk_image, sym2_iInter, sym2_image, sym2_insert, sym2_inter, sym2_preimage, sym2_singleton, sym2_univ, map, mem_range_diag, is_equivalence, trans, add_mk, attachWith_map_subtypeVal, ball, card_toFinset, card_toFinset_of_isDiag, card_toFinset_of_not_isDiag, card_toMultiset, coe_lift_symm_apply, coe_lift₂_symm_apply, coe_mk, congr_left, congr_right, diagSet_compl_eq_fromRel_ne, diagSet_compl_eq_setOf_not_isDiag, diagSet_eq_fromRel_eq, diagSet_eq_setOf_isDiag, diagSet_eq_univ_of_subsingleton, diagSet_subset_fromRel, diag_injective, diag_isDiag, disjoint_diagSet_fromRel, eq, eq_iff, eq_of_ne_mem, eq_swap, exact, exists, ext, ext_iff, filter_image_mk_isDiag, filter_image_mk_not_isDiag, forall, forall_mem_pair, fromRel_bot, fromRel_bot_iff, fromRel_eq_fromRell_iff_eq, fromRel_irrefl, fromRel_irreflexive, fromRel_mono, fromRel_mono_iff, fromRel_ne, fromRel_proj_prop, fromRel_prop, fromRel_relationMap, fromRel_subset_compl_diagSet, fromRel_toRel, fromRel_top, fromRel_top_iff, ind, inductionOn, inductionOn₂, instIsEmpty, instNontrivial, instSubsingleton, irreflexive_iff_fromRel_subset_diagSet_compl, isDiag_iff_mem_range_diag, isDiag_iff_proj_eq, isDiag_map, isDiag_of_subsingleton, lift_comp_map, lift_map_apply, lift_mk, lift_smul_lift, lift₂_mk, injective, map_comp, map_congr, map_id, map_id', map_map, map_mk, map_pair_eq, map_pmap, mem_and_mem_iff, mem_diagSet, mem_diagSet_iff_eq, mem_diagSet_iff_isDiag, mem_fromRel_irrefl_other_ne, mem_iff, mem_iff', mem_iff_exists, mem_iff_mem, mem_map, mem_mk_left, mem_mk_right, mem_pmap_iff, mem_toFinset, mem_toMultiset, mkEmbedding_apply, mk_eq_mk_iff, mk_isDiag_iff, mk_prod_swap_eq, mk_surjective, mul_mk, other_eq_other', other_invol, other_invol', other_mem, other_mem', other_ne, other_spec, other_spec', out_fst_mem, out_snd_mem, pair_eq_pmap, pmap_eq_map, pmap_map, pmap_pair, pmap_pmap, pmap_subtype_map_subtypeVal, range_diag, reflexive_iff_diagSet_subset_fromRel, rel_iff, rel_iff', sound, toFinset_mk_eq, toRel_fromRel, toRel_prop, toRel_symmetric	137
Total	177

Function.Embedding

Definitions

Name	Category	Theorems
sym2Map 📖	CompOp	6 math math: SimpleGraph.map_edgeFinset_induce_of_support_subset, SimpleGraph.edgeFinset_map, Finset.sym2_map, sym2Map_apply, SimpleGraph.edgeSet_map, SimpleGraph.map_edgeFinset_induce

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sym2Map_apply 📖	mathematical	—	DFunLike.coe Function.Embedding Sym2 Function.instFunLikeEmbedding sym2Map Sym2.map	—	—

Set

Definitions

Name	Category	Theorems
sym2 📖	CompOp	16 math math: List.setOf_mem_sym2, sym2_eq_mk_image, sym2_preimage, Multiset.setOf_mem_sym2, sym2_image, mk'_mem_sym2_iff, sym2_insert, sym2_iInter, mem_sym2_iff_subset, sym2_inter, Finset.coe_sym2, mk_mem_sym2_iff, sym2_univ, sym2_empty, mk_preimage_sym2, sym2_singleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_sym2_iff_subset 📖	mathematical	—	Sym2 Set instMembership sym2 instHasSubset SetLike.coe Sym2.instSetLike	—	Sym2.inductionOn
mk'_mem_sym2_iff 📖	mathematical	—	Sym2 Set instMembership sym2	—	mk_mem_sym2_iff
mk_mem_sym2_iff 📖	mathematical	—	Sym2 Set instMembership sym2	—	—
mk_preimage_sym2 📖	mathematical	—	preimage Sym2 sym2 SProd.sprod Set instSProd	—	—
sym2_empty 📖	mathematical	—	sym2 Set instEmptyCollection Sym2	—	ext
sym2_eq_mk_image 📖	mathematical	—	sym2 image Sym2 SProd.sprod Set instSProd	—	ext image_uncurry_prod image2_curry
sym2_iInter 📖	mathematical	—	sym2 iInter Sym2	—	ext
sym2_image 📖	mathematical	—	sym2 image Sym2 Sym2.map	—	sym2_eq_mk_image prod_image_image_eq image_image image_congr
sym2_insert 📖	mathematical	—	sym2 Set instInsert Sym2 instUnion image	—	ext
sym2_inter 📖	mathematical	—	sym2 Set instInter Sym2	—	preimage_injective Sym2.mk_surjective prod_inter_prod
sym2_preimage 📖	mathematical	—	sym2 preimage Sym2 Sym2.map	—	ext
sym2_singleton 📖	mathematical	—	sym2 Set instSingletonSet Sym2	—	ext
sym2_univ 📖	mathematical	—	sym2 univ Sym2	—	ext

Sym2

Definitions

Name	Category	Theorems
ToRel 📖	MathDef	5 math math: toRel_prop, SimpleGraph.reachable_fromEdgeSet_eq_reflTransGen_toRel, fromRel_toRel, toRel_symmetric, toRel_fromRel
add 📖	CompOp	1 math math: add_mk
attachWith 📖	CompOp	1 math math: attachWith_map_subtypeVal
decidablePred_mem_diagSet 📖	CompOp	2 math math: SimpleGraph.edgeFinset_top, card_diagSet_compl
diag 📖	CompOp	6 math math: diag_injective, range_diag, diag_isDiag, Finset.diag_mem_sym2_iff, isDiag_iff_mem_range_diag, Finset.sym2_singleton
diagSet 📖	CompOp	25 math math: disjoint_diagSet_fromRel, SimpleGraph.edgeSet_fromEdgeSet, diagSet_subset_fromRel, reflexive_iff_diagSet_subset_fromRel, SimpleGraph.edgeFinset_top, SimpleGraph.edgeSet_top, SimpleGraph.edgeSet_eq_iff, diagSet_eq_setOf_isDiag, SimpleGraph.fromEdgeSet_not_isDiag, diagSet_eq_fromRel_eq, range_diag, diagSet_compl_eq_fromRel_ne, SimpleGraph.edgeSet_sdiff_sdiff_isDiag, SimpleGraph.fromEdgeSet_le, card_diagSet_compl, fromRel_subset_compl_diagSet, diagSet_compl_eq_setOf_not_isDiag, SimpleGraph.edgeSet_subset_setOf_not_isDiag, irreflexive_iff_fromRel_subset_diagSet_compl, mem_diagSet, IsDiag.mem_range_diag, SimpleGraph.edgeSet_subset_compl_diagSet, diagSet_eq_univ_of_subsingleton, mem_diagSet_iff_eq, mem_diagSet_iff_isDiag
equivMultiset 📖	CompOp	—
equivSym 📖	CompOp	1 math math: List.sym2_eq_sym_two
fromRel 📖	CompOp	21 math math: disjoint_diagSet_fromRel, diagSet_subset_fromRel, reflexive_iff_diagSet_subset_fromRel, fromRel_relationMap, fromRel_ne, fromRel_top, fromRel_mono_iff, fromRel_bot_iff, diagSet_eq_fromRel_eq, fromRel_toRel, diagSet_compl_eq_fromRel_ne, fromRel_eq_fromRell_iff_eq, fromRel_subset_compl_diagSet, fromRel_bot, fromRel_prop, irreflexive_iff_fromRel_subset_diagSet_compl, toRel_fromRel, fromRel_proj_prop, fromRel_mono, SimpleGraph.reachable_fromEdgeSet_fromRel_eq_reflTransGen, fromRel_top_iff
fromRelOrderEmbedding 📖	CompOp	—
hrec 📖	CompOp	—
instDecidableEq 📖	CompOp	28 math math: SimpleGraph.Dart.edge_fiber, SimpleGraph.edgeFinset_sdiff, SimpleGraph.dart_edge_fiber_card, filter_image_mk_isDiag, Finset.sym2_toFinset, SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff, SimpleGraph.edgeFinset_replaceVertex_of_adj, card_image_diag, SimpleGraph.edgeFinset_replaceVertex_of_not_adj, SimpleGraph.Path.count_edges_eq_one, SimpleGraph.Walk.IsTrail.count_edges_eq_one, SimpleGraph.edgeFinset_sup, SimpleGraph.Walk.IsTrail.count_edges_le_one, Finset.image_diag_union_image_offDiag, filter_image_mk_not_isDiag, Finset.sym2_insert, card_image_offDiag, Multiset.dedup_sym2, SimpleGraph.disjoint_sdiff_neighborFinset_image, SimpleGraph.Walk.count_edges_takeUntil_le_one, SimpleGraph.Walk.coe_edges_toFinset, two_mul_card_image_offDiag, List.dedup_sym2, Finset.sym2_image, SimpleGraph.edgeFinset_deleteEdges, SimpleGraph.edgeFinset_inf, SimpleGraph.map_edgeFinset_induce, Finset.sym2_eq_image
instDecidableRel 📖	CompOp	—
instDecidableRel' 📖	CompOp	—
instPartialOrder 📖	CompOp	—
instRepr 📖	CompOp	—
instSetLike 📖	CompOp	27 math math: mem_mk_right, SimpleGraph.incidenceFinset_eq_filter, mem_pmap_iff, mem_mk_left, mem_and_mem_iff, SimpleGraph.Walk.IsTrail.even_countP_edges_iff, SimpleGraph.edge_mem_incidenceSet_iff, out_fst_mem, coe_mk, SimpleGraph.edgeFinset_deleteIncidenceSet_eq_filter, mem_iff_exists, ext_iff, mem_toFinset, mem_iff, mem_toMultiset, pmap_map, map_pmap, Set.mem_sym2_iff_subset, SimpleGraph.Walk.mem_support_iff_exists_mem_edges_of_not_nil, mem_map, SimpleGraph.lineGraph_adj_iff_exists, pmap_pmap, SimpleGraph.IsIndepSet.nonempty_mem_compl_mem_edge, SimpleGraph.adj_iff_exists_edge, out_snd_mem, SimpleGraph.Walk.mem_support_iff_exists_mem_edges, mem_iff_mem
instUnique 📖	CompOp	—
lift₂ 📖	CompOp	2 math math: lift₂_mk, coe_lift₂_symm_apply
map 📖	CompOp	47 math math: map.injective, QuadraticMap.sum_polar_sub_repr_sq, IsDiag.map, Set.sym2_preimage, fromRel_relationMap, lift_comp_map, SimpleGraph.Subgraph.image_coe_edgeSet_coe, pmap_subtype_map_subtypeVal, QuadraticMap.map_finsuppSum, SimpleGraph.Embedding.map_mem_edgeSet_iff, Set.sym2_image, attachWith_map_subtypeVal, SimpleGraph.Iso.map_mem_edgeSet_iff, map_id', map_map, SimpleGraph.Hom.mapEdgeSet_coe, SimpleGraph.Hom.map_mem_edgeSet, pmap_eq_map, List.sym2_map, Function.Embedding.sym2Map_apply, SimpleGraph.Subgraph.deleteEdges_coe_eq, SimpleGraph.Subgraph.edgeSet_map, QuadraticMap.map_finsuppSum', map_mk, map_comp, QuadraticMap.map_sum', Finsupp.coe_sym2Mul, pmap_map, map_pmap, QuadraticMap.apply_linearCombination', map_id, SimpleGraph.Subgraph.edgeSet_coe, mem_map, SimpleGraph.Walk.edgeSet_map, QuadraticMap.apply_linearCombination, QuadraticMap.map_sum, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, SimpleGraph.Walk.edges_map, QuadraticMap.polarSym2_map_smul, Multiset.sym2_map, isDiag_map, Finset.sym2_image, map_pair_eq, lift_map_apply, map_congr, SimpleGraph.Subgraph.coe_deleteEdges_eq, Finsupp.sym2_support_eq_preimage_support_mul
mk 📖	CompOp	—
mkEmbedding 📖	CompOp	2 math math: mkEmbedding_apply, Finset.sym2_cons
mul 📖	CompOp	6 math math: mul_mk, Finsupp.coe_sym2Mul, QuadraticMap.apply_linearCombination, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, QuadraticMap.polarSym2_map_smul, Finsupp.sym2_support_eq_preimage_support_mul
pmap 📖	CompOp	8 math math: pmap_subtype_map_subtypeVal, mem_pmap_iff, pmap_eq_map, pmap_pair, pmap_map, map_pmap, pair_eq_pmap, pmap_pmap
rec 📖	CompOp	—
recOn 📖	CompOp	—
recOnSubsingleton 📖	CompOp	—
sym2EquivSym' 📖	CompOp	—
toFinset 📖	CompOp	6 math math: card_toFinset_of_not_isDiag, toFinset_mk_eq, card_toFinset_of_isDiag, mem_toFinset, card_toFinset, SimpleGraph.card_toFinset_mem_edgeFinset
toMultiset 📖	CompOp	2 math math: card_toMultiset, mem_toMultiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mk 📖	mathematical	—	add AddCommMagma.toAdd	—	—
attachWith_map_subtypeVal 📖	mathematical	—	map attachWith	—	ind
ball 📖	—	—	—	—	—
card_toFinset 📖	mathematical	—	Finset.card toFinset IsDiag IsDiag.decidablePred	—	card_toFinset_of_isDiag card_toFinset_of_not_isDiag
card_toFinset_of_isDiag 📖	mathematical	IsDiag	Finset.card toFinset	—	ind mk_isDiag_iff toFinset_mk_eq Finset.insert_eq_of_mem Finset.card_singleton
card_toFinset_of_not_isDiag 📖	mathematical	IsDiag	Finset.card toFinset	—	ind toFinset_mk_eq Finset.card_insert_of_notMem mk_isDiag_iff Finset.card_singleton
card_toMultiset 📖	mathematical	—	Multiset.card toMultiset	—	ind zero_add
coe_lift_symm_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift	—	—
coe_lift₂_symm_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift₂	—	—
coe_mk 📖	mathematical	—	SetLike.coe Sym2 instSetLike Set Set.instInsert Set.instSingletonSet	—	Set.ext
congr_left 📖	—	—	—	—	—
congr_right 📖	—	—	—	—	—
diagSet_compl_eq_fromRel_ne 📖	mathematical	—	Compl.compl Set Sym2 Set.instCompl diagSet fromRel	—	Set.ext
diagSet_compl_eq_setOf_not_isDiag 📖	mathematical	—	Compl.compl Set Sym2 Set.instCompl diagSet setOf IsDiag	—	diagSet_eq_setOf_isDiag
diagSet_eq_fromRel_eq 📖	mathematical	—	diagSet fromRel Equivalence.symmetric eq_equivalence	—	Set.ext Equivalence.symmetric eq_equivalence
diagSet_eq_setOf_isDiag 📖	mathematical	—	diagSet setOf Sym2 IsDiag	—	—
diagSet_eq_univ_of_subsingleton 📖	mathematical	—	diagSet Set.univ Sym2	—	Set.ext
diagSet_subset_fromRel 📖	mathematical	Symmetric	Set Sym2 Set.instHasSubset diagSet fromRel Reflexive	—	—
diag_injective 📖	mathematical	—	Sym2 diag	—	exact
diag_isDiag 📖	mathematical	—	IsDiag diag	—	—
disjoint_diagSet_fromRel 📖	mathematical	Symmetric	Disjoint Set Sym2 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra diagSet fromRel	—	—
eq 📖	mathematical	—	Rel	—	Quotient.eq'
eq_iff 📖	—	—	—	—	—
eq_of_ne_mem 📖	—	Sym2 SetLike.instMembership instSetLike	—	—	mem_and_mem_iff
eq_swap 📖	—	—	—	—	—
exact 📖	mathematical	—	Rel	—	—
exists 📖	—	—	—	—	Function.Surjective.exists mk_surjective
ext 📖	—	Sym2 SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike	—	ext
filter_image_mk_isDiag 📖	mathematical	—	Finset.filter Sym2 IsDiag IsDiag.decidablePred Finset.image instDecidableEq SProd.sprod Finset Finset.instSProd Finset.diag	—	Finset.image_diag Finset.ext
filter_image_mk_not_isDiag 📖	mathematical	—	Finset.filter Sym2 IsDiag IsDiag.decidablePred Finset.image instDecidableEq SProd.sprod Finset Finset.instSProd Finset.offDiag	—	Finset.ext
forall 📖	—	—	—	—	Function.Surjective.forall mk_surjective
forall_mem_pair 📖	—	—	—	—	—
fromRel_bot 📖	mathematical	—	fromRel Bot.bot Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra Set Sym2 Set.instEmptyCollection	—	Set.eq_empty_of_forall_notMem ind
fromRel_bot_iff 📖	mathematical	Symmetric	fromRel Set Sym2 Set.instEmptyCollection Bot.bot Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	fromRel_prop fromRel_bot
fromRel_eq_fromRell_iff_eq 📖	mathematical	Symmetric	fromRel	—	OrderEmbedding.eq_iff_eq
fromRel_irrefl 📖	mathematical	Symmetric	IsDiag	—	ind fromRel_prop
fromRel_irreflexive 📖	mathematical	Symmetric	IsDiag	—	fromRel_irrefl
fromRel_mono 📖	mathematical	Symmetric Pi.hasLe Prop.le	Set Sym2 Set.instHasSubset fromRel	—	fromRel_mono_iff
fromRel_mono_iff 📖	mathematical	Symmetric	Set Sym2 Set.instHasSubset fromRel Pi.hasLe Prop.le	—	ind
fromRel_ne 📖	mathematical	—	fromRel setOf Sym2 IsDiag	—	Set.ext ind
fromRel_proj_prop 📖	mathematical	Symmetric	Sym2 Set Set.instMembership fromRel	—	fromRel_prop
fromRel_prop 📖	mathematical	Symmetric	Sym2 Set Set.instMembership fromRel	—	—
fromRel_relationMap 📖	mathematical	Symmetric	fromRel Relation.Map Relation.map_symmetric Set.image Sym2 map	—	Set.ext Relation.map_symmetric
fromRel_subset_compl_diagSet 📖	mathematical	Symmetric	Set Sym2 Set.instHasSubset fromRel Compl.compl Set.instCompl diagSet	—	—
fromRel_toRel 📖	mathematical	—	fromRel ToRel toRel_symmetric	—	Set.ext toRel_symmetric ind
fromRel_top 📖	mathematical	—	fromRel Top.top Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra Set.univ Sym2	—	Set.eq_univ_of_forall ind
fromRel_top_iff 📖	mathematical	Symmetric	fromRel Set.univ Sym2 Top.top Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	fromRel_prop fromRel_top
ind 📖	—	—	—	—	—
inductionOn 📖	—	—	—	—	ind
inductionOn₂ 📖	—	—	—	—	Quot.induction_on₂
instIsEmpty 📖	mathematical	—	IsEmpty Sym2	—	Equiv.isEmpty Sym.instIsEmptySucc
instNontrivial 📖	mathematical	—	Nontrivial Sym2	—	Function.Injective.nontrivial diag_injective
instSubsingleton 📖	mathematical	—	Sym2	—	Function.Injective.subsingleton Equiv.injective Sym.instSubsingleton
irreflexive_iff_fromRel_subset_diagSet_compl 📖	mathematical	Symmetric	Set Sym2 Set.instHasSubset fromRel Compl.compl Set.instCompl diagSet	—	—
isDiag_iff_mem_range_diag 📖	mathematical	—	IsDiag Sym2 Set Set.instMembership Set.range diag	—	range_diag
isDiag_iff_proj_eq 📖	mathematical	—	IsDiag	—	mk_isDiag_iff
isDiag_map 📖	mathematical	—	IsDiag map	—	ind
isDiag_of_subsingleton 📖	mathematical	—	IsDiag	—	ind
lift_comp_map 📖	mathematical	—	Sym2 DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike lift map Subtype.prop	—	Subtype.prop Equiv.symm_apply_eq
lift_map_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike lift map Subtype.prop	—	Subtype.prop lift_comp_map
lift_mk 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike lift	—	—
lift_smul_lift 📖	mathematical	—	Pi.smul' Sym2 DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike lift	—	—
lift₂_mk 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike lift₂	—	—
map_comp 📖	mathematical	—	map Sym2	—	—
map_congr 📖	mathematical	—	map	—	ext
map_id 📖	mathematical	—	map Sym2	—	—
map_id' 📖	mathematical	—	map Sym2	—	map_id
map_map 📖	mathematical	—	map	—	ind
map_mk 📖	mathematical	—	map	—	—
map_pair_eq 📖	mathematical	—	map	—	—
map_pmap 📖	mathematical	—	pmap map Sym2 SetLike.instMembership instSetLike mem_map	—	ind mem_map
mem_and_mem_iff 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike	—	ind mem_iff
mem_diagSet 📖	mathematical	—	Sym2 Set Set.instMembership diagSet IsDiag	—	—
mem_diagSet_iff_eq 📖	mathematical	—	Sym2 Set Set.instMembership diagSet	—	—
mem_diagSet_iff_isDiag 📖	mathematical	—	Sym2 Set Set.instMembership diagSet IsDiag	—	—
mem_fromRel_irrefl_other_ne 📖	—	Symmetric Sym2 Set Set.instMembership fromRel SetLike.instMembership instSetLike	—	—	other_ne fromRel_irrefl
mem_iff 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike	—	mem_iff'
mem_iff' 📖	mathematical	—	Mem	—	eq_iff eq_swap
mem_iff_exists 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike	—	—
mem_iff_mem 📖	mathematical	—	Mem Sym2 SetLike.instMembership instSetLike	—	—
mem_map 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike map	—	ind
mem_mk_left 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike	—	—
mem_mk_right 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike	—	mem_mk_left eq_swap
mem_pmap_iff 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike pmap	—	mem_mk_left mem_mk_right pmap_pair
mem_toFinset 📖	mathematical	—	Finset Finset.instMembership toFinset Sym2 SetLike.instMembership instSetLike	—	mem_toMultiset toFinset.eq_1 Multiset.mem_toFinset
mem_toMultiset 📖	mathematical	—	Multiset Multiset.instMembership toMultiset Sym2 SetLike.instMembership instSetLike	—	ind
mkEmbedding_apply 📖	mathematical	—	DFunLike.coe Function.Embedding Sym2 Function.instFunLikeEmbedding mkEmbedding	—	—
mk_eq_mk_iff 📖	—	—	—	—	—
mk_isDiag_iff 📖	mathematical	—	IsDiag	—	—
mk_prod_swap_eq 📖	—	—	—	—	eq_swap
mk_surjective 📖	mathematical	—	Sym2	—	Quot.mk_surjective
mul_mk 📖	mathematical	—	mul CommMagma.toMul	—	—
other_eq_other' 📖	mathematical	Sym2 SetLike.instMembership instSetLike	Mem.other Mem.other'	—	congr_right other_spec' other_spec
other_invol 📖	—	Sym2 SetLike.instMembership instSetLike Mem.other	—	—	other_eq_other' other_invol'
other_invol' 📖	—	Sym2 SetLike.instMembership instSetLike Mem.other'	—	—	ind
other_mem 📖	mathematical	Sym2 SetLike.instMembership instSetLike	Mem.other	—	other_spec mem_mk_right
other_mem' 📖	mathematical	Sym2 SetLike.instMembership instSetLike	Mem.other'	—	other_eq_other' other_mem
other_ne 📖	—	IsDiag Sym2 SetLike.instMembership instSetLike	—	—	Mathlib.Tactic.Contrapose.contrapose₄ other_spec
other_spec 📖	mathematical	Sym2 SetLike.instMembership instSetLike	Mem.other	—	—
other_spec' 📖	mathematical	Sym2 SetLike.instMembership instSetLike	Mem.other'	—	ind instIsEmptyFalse
out_fst_mem 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike Quot.out Rel	—	Quot.out_eq
out_snd_mem 📖	mathematical	—	Sym2 SetLike.instMembership instSetLike Quot.out Rel	—	eq_swap Quot.out_eq
pair_eq_pmap 📖	mathematical	—	pmap forall_mem_pair	—	—
pmap_eq_map 📖	mathematical	—	pmap map	—	ind
pmap_map 📖	mathematical	—	map pmap Sym2 SetLike.instMembership instSetLike	—	ind
pmap_pair 📖	mathematical	—	pmap mem_mk_left mem_mk_right	—	—
pmap_pmap 📖	mathematical	—	pmap Sym2 SetLike.instMembership instSetLike mem_pmap_iff	—	ind mem_pmap_iff
pmap_subtype_map_subtypeVal 📖	mathematical	—	map pmap	—	ind
range_diag 📖	mathematical	—	Set.range Sym2 diag diagSet	—	Set.ext
reflexive_iff_diagSet_subset_fromRel 📖	mathematical	Symmetric	Reflexive Set Sym2 Set.instHasSubset diagSet fromRel	—	—
rel_iff 📖	mathematical	—	Rel	—	—
rel_iff' 📖	mathematical	—	Rel	—	—
sound 📖	—	Rel	—	—	—
toFinset_mk_eq 📖	mathematical	—	toFinset Finset Finset.instInsert Finset.instSingleton	—	Finset.ext
toRel_fromRel 📖	mathematical	Symmetric	ToRel fromRel	—	—
toRel_prop 📖	mathematical	—	ToRel Sym2 Set Set.instMembership	—	—
toRel_symmetric 📖	mathematical	—	Symmetric ToRel	—	eq_swap

Sym2.IsDiag

Definitions

Name	Category	Theorems
decidablePred 📖	CompOp	10 math math: Sym2.card_subtype_not_diag, Sym2.filter_image_mk_isDiag, QuadraticMap.map_finsuppSum, Sym2.filter_image_mk_not_isDiag, Sym2.card_toFinset, QuadraticMap.apply_linearCombination, Sym2.card_subtype_diag, Finset.sum_sym2_filter_not_isDiag, QuadraticMap.map_sum, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	Sym2.IsDiag	Sym2.map	—	Sym2.ind
mem_range_diag 📖	mathematical	Sym2.IsDiag	Sym2 Set Set.instMembership Sym2.diagSet	—	Sym2.mem_diagSet_iff_isDiag

Sym2.Mem

Definitions

Name	Category	Theorems
decidable 📖	CompOp	3 math math: SimpleGraph.incidenceFinset_eq_filter, SimpleGraph.Walk.IsTrail.even_countP_edges_iff, SimpleGraph.edgeFinset_deleteIncidenceSet_eq_filter
other 📖	CompOp	4 math math: SimpleGraph.adj_incidenceSet_inter, Sym2.other_mem, Sym2.other_spec, Sym2.other_eq_other'
other' 📖	CompOp	3 math math: Sym2.other_eq_other', Sym2.other_spec', Sym2.other_mem'

Sym2.Rel

Definitions

Name	Category	Theorems
setoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
is_equivalence 📖	mathematical	—	Sym2.Rel	—	symm trans
trans 📖	—	Sym2.Rel	—	—	—

Sym2.fromRel

Definitions

Name	Category	Theorems
decidablePred 📖	CompOp	—

Sym2.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	mathematical	—	Sym2 Sym2.map	—	Sym2.inductionOn₂

(root)

Definitions

Name	Category	Theorems
Sym2 📖	CompOp	419 math math: SimpleGraph.Walk.isEulerian_iff, List.setOf_mem_sym2, SimpleGraph.edgeFinset_mono, SimpleGraph.not_mem_edgeSet_of_isDiag, Sym2.map.injective, SimpleGraph.mem_incidenceSet, SimpleGraph.deleteFar_iff, SimpleGraph.incidenceSetEquivNeighborSet_apply_coe, SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le, Sym2.disjoint_diagSet_fromRel, Finset.mk_mem_sym2_iff, Set.sym2_eq_mk_image, SimpleGraph.incidenceSet_inter_incidenceSet_of_adj, SimpleGraph.Connected.connected_delete_edge_of_not_isBridge, SimpleGraph.fromEdgeSet_inter, QuadraticMap.sum_polar_sub_repr_sq, SimpleGraph.edgeFinset_subset_sym2_of_support_subset, SimpleGraph.edgeSet_fromEdgeSet, SimpleGraph.Walk.edges_take, SimpleGraph.DeleteFar.le_card_sub_card, SimpleGraph.two_mul_card_edgeFinset, SimpleGraph.sum_degrees_eq_twice_card_edges, Multiset.Nodup.sym2, Sym2.card_subtype_not_diag, Sym2.mem_mk_right, SimpleGraph.Walk.edges_eq_zipWith_support, SimpleGraph.adj_iff_exists_edge_coe, SimpleGraph.sum_incMatrix_apply, Sym2.diagSet_subset_fromRel, SimpleGraph.Walk.edges_concat, SimpleGraph.Dart.edge_fiber, Set.sym2_preimage, SimpleGraph.isEdgeConnected_two, SimpleGraph.edgeFinset_sdiff, SimpleGraph.subgraphOfAdj_adj, SimpleGraph.card_edgeFinset_sup_edge, SimpleGraph.incMatrix_apply_mul_incMatrix_apply, SimpleGraph.Walk.edges_nodup_of_support_nodup, SimpleGraph.incidenceSet_inter_incidenceSet_of_not_adj, Sym2.reflexive_iff_diagSet_subset_fromRel, Sym2.fromRel_relationMap, SimpleGraph.edgeFinset_top, SimpleGraph.Walk.head_edges_eq_mk_start_snd, SimpleGraph.map_edgeFinset_induce_of_support_subset, SimpleGraph.IsAcyclic.isPath_iff_isChain, SimpleGraph.extremalNumber_le_iff_of_nonneg, SimpleGraph.Subgraph.spanningCoe_subgraphOfAdj, Sym2.lift_comp_map, Sym2.instNontrivial, Sym2.filter_image_mk_isDiag, SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj, SimpleGraph.Walk.IsTrail.edges_nodup, SimpleGraph.card_edgeFinset_le_card_choose_two, Sym2.sortEquiv_apply_coe, SimpleGraph.isEdgeReachable_add_one, Sym2.fromRel_ne, SimpleGraph.incidenceFinset_eq_filter, Finset.sym2_toFinset, SimpleGraph.card_edgeFinset_map, SimpleGraph.farFromTriangleFree_iff, SimpleGraph.card_incidenceSet_eq_degree, SimpleGraph.Walk.rotate_edges, SimpleGraph.Subgraph.image_coe_edgeSet_coe, SimpleGraph.Subgraph.edgeSet_bot, List.length_sym2, SimpleGraph.Walk.cons_isCycle_iff, List.Perm.sym2, SimpleGraph.Subgraph.mem_edgeSet, SimpleGraph.deleteEdges_fromEdgeSet, SimpleGraph.coe_edgeFinset, SimpleGraph.edgeSet_top, SimpleGraph.deleteEdges_univ, SimpleGraph.Walk.isTrail_def, SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff, Sym2.fromRel_top, Sym2.fromRel_mono_iff, SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges, List.Sublist.sym2, SimpleGraph.edgeFinset_map, SimpleGraph.isEdgeConnected_add_one, SimpleGraph.card_edgeFinset_of_isExtremal_free, Sym2.diag_injective, Sym2.mem_pmap_iff, SimpleGraph.Walk.mk_start_snd_eq_head_edges, SimpleGraph.mem_incidenceFinset, SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges', Sym2.mkEmbedding_apply, SimpleGraph.edgeSet_ssubset_edgeSet, SimpleGraph.edgeFinset_replaceVertex_of_adj, SimpleGraph.edgeSet_replaceVertex_of_adj, SimpleGraph.LocallyLinear.card_edgeFinset, QuadraticMap.map_finsuppSum, Multiset.setOf_mem_sym2, SimpleGraph.edgeFinset_nonempty, SimpleGraph.reachable_delete_edges_iff_exists_walk, SimpleGraph.Embedding.map_mem_edgeSet_iff, SimpleGraph.edge_edgeSet_of_ne, SimpleGraph.edgeSet_eq_iff, SimpleGraph.card_edgeFinset_le_extremalNumber, Finset.card_sym2, SimpleGraph.edgeSet_bot, SimpleGraph.farFromTriangleFree.le_card_sub_card, SimpleGraph.edgeSet_inf, SimpleGraph.Walk.edgeSet_nil, SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle, SimpleGraph.disjoint_edgeFinset, List.Nodup.sym2, SimpleGraph.isExtremal_free_iff, SimpleGraph.incMatrix_apply', SimpleGraph.edgeSet_subset_edgeSet, SimpleGraph.card_edgeFinset_turanGraph_add, Sym2.card_image_diag, SimpleGraph.le_card_edgeFinset_killCopies_add_copyCount, SimpleGraph.Subgraph.edgeSet_iInf, Set.sym2_image, Sym2.diagSet_eq_setOf_isDiag, SimpleGraph.edgeFinset_replaceVertex_of_not_adj, SimpleGraph.disjoint_edgeSet, SimpleGraph.Iso.map_mem_edgeSet_iff, Sym2.fromRel_bot_iff, Multiset.mk_mem_sym2_iff, SimpleGraph.isEdgeReachable_two, Sym2.toRel_prop, Multiset.sym2_eq_zero_iff, SimpleGraph.fromEdgeSet_not_isDiag, SimpleGraph.Subgraph.IsMatching.toEdge.surjective, Sym2.map_id', SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges, SimpleGraph.edgeSet_deleteIncidenceSet, Sym2.mem_mk_left, SimpleGraph.Hom.mapEdgeSet_coe, SimpleGraph.Iso.card_edgeFinset_eq, SimpleGraph.isTree_iff_connected_and_card, SimpleGraph.fromEdgeSet_adj, List.mk_mem_sym2, Finset.mem_sym2_iff, SimpleGraph.incidenceFinset_subset, SimpleGraph.vertexCoverNum_le_encard_edgeSet, Finset.sym2_mono, SimpleGraph.Walk.edges_takeUntil_subset, Finset.sym2_map, Sym2.mem_and_mem_iff, SimpleGraph.extremalNumber_top, SimpleGraph.edgeFinset_sup, SimpleGraph.Walk.IsTrail.even_countP_edges_iff, SimpleGraph.card_edgeFinset_deleteIncidenceSet_le_extremalNumber, SimpleGraph.Subgraph.deleteEdges_empty_eq, Set.mk'_mem_sym2_iff, SimpleGraph.edgeSet_subgraphOfAdj, SimpleGraph.fromEdgeSet_sdiff, Multiset.mem_sym2_iff, SimpleGraph.Walk.edgeSet_concat, SimpleGraph.edge_mem_incidenceSet_iff, Sym2.range_diag, SimpleGraph.incidenceSetEquivNeighborSet_symm_apply_coe, List.sym2_map, SimpleGraph.Walk.IsTrail.count_edges_le_one, Function.Embedding.sym2Map_apply, SimpleGraph.card_edgeFinset_top_eq_card_choose_two, SimpleGraph.dart_card_eq_twice_card_edges, SimpleGraph.fromEdgeSet_univ, Sym2.out_fst_mem, SimpleGraph.Walk.edges_dropUntil_subset, Finsupp.support_sym2Mul_subset, SimpleGraph.Walk.edges_nil, SimpleGraph.Subgraph.deleteEdges_coe_eq, SimpleGraph.Subgraph.edgeSet_map, SimpleGraph.edgeSet_nonempty, SimpleGraph.Hom.mapEdgeSet.injective, Sym2.diagSet_compl_eq_fromRel_ne, SimpleGraph.incMatrix_mul_transpose, SimpleGraph.Walk.mem_edgeSet, SimpleGraph.incMatrix_apply_eq_one_iff, SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_right_eq, SimpleGraph.Walk.exists_mem_edges_of_not_reachable_deleteEdges, SimpleGraph.Walk.infix_support_iff_mem_edges, SimpleGraph.Subgraph.edgeSet_mono, Sym2.coe_mk, SimpleGraph.Subgraph.edgeSet_sInf, SimpleGraph.mem_incidence_iff_neighbor, SimpleGraph.edgeSet_sdiff_sdiff_isDiag, SimpleGraph.extremalNumber_of_fintypeCard_eq, SimpleGraph.DeleteFar.le_card_edgeFinset, SimpleGraph.Subgraph.edgeSet_sSup, Finset.sym2_empty, SimpleGraph.Path.notMem_edges_of_loop, SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one, SimpleGraph.incidenceSet_inter_incidenceSet_subset, SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_left_eq, QuadraticMap.map_finsuppSum', SimpleGraph.edgeFinset_deleteIncidenceSet_eq_filter, Sym2.mk_surjective, SimpleGraph.Walk.edges_cycleBypass_subset, SimpleGraph.fromEdgeSet_le, SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton, SimpleGraph.Dart.edge_comp_symm, Finset.sym2_nonempty, SimpleGraph.edgeFinset_strict_mono, SimpleGraph.Walk.toSubgraph_le_iff, SimpleGraph.deleteEdges_adj, Multiset.sym2_zero, SimpleGraph.Walk.mk_penultimate_end_eq_getLast_edges, SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj, Sym2.mem_iff_exists, SimpleGraph.isBridge_iff, SimpleGraph.Subgraph.deleteEdges_adj, List.mk_mem_sym2_iff, SimpleGraph.Subgraph.edgeSet_iSup, Sym2.ext_iff, SimpleGraph.coe_incidenceFinset, Set.sym2_insert, Sym2.sortEquiv_symm_apply, Sym2.card_diagSet_compl, Finset.sym2_cons, SimpleGraph.edgeSet_strict_mono, SimpleGraph.le_card_edgeFinset_killCopies, Sym2.mem_toFinset, SimpleGraph.card_edgeFinset_replaceVertex_of_adj, SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem, SimpleGraph.Walk.edges_cons, Finset.Nonempty.sym2, Sym2.mem_iff, SimpleGraph.fromEdgeSet_disjoint, Finset.sym2_univ, Multiset.sym2_mono, SimpleGraph.Subgraph.edgeSet_subset, SimpleGraph.fromEdgeSet_empty, Sym2.fromRel_subset_compl_diagSet, Sym2.map_comp, Multiset.sym2_cons, Finset.injective_sym2, Sym2.mem_toMultiset, Finset.diag_mem_sym2_iff, Sym2.lift_smul_lift, SimpleGraph.deleteEdges_empty, Sym2.isDiag_iff_mem_range_diag, Sym2.fromRel_bot, QuadraticMap.map_sum', Finsupp.coe_sym2Mul, SimpleGraph.lineGraph_bot, SimpleGraph.deleteEdges_eq_inter_edgeSet, SimpleGraph.sum_degrees_support_eq_twice_card_edges, Sym2.diagSet_compl_eq_setOf_not_isDiag, SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton, Finset.image_diag_union_image_offDiag, SimpleGraph.incMatrix_mul_transpose_diag, Sym2.pmap_map, SimpleGraph.edgeSet_mono, Set.sym2_iInter, Sym2.filter_image_mk_not_isDiag, SimpleGraph.Subgraph.edgeSet_sup, Sym2.instIsEmpty, List.map_mk_disjoint_sym2, SimpleGraph.Walk.edges_bypass_subset, SimpleGraph.mem_edgeFinset, Sym2.map_pmap, SimpleGraph.edgeFinset_bot, SimpleGraph.extremalNumber_le_iff, Set.mem_sym2_iff_subset, Finset.monotone_sym2, SimpleGraph.card_edgeFinset_deleteIncidenceSet, SimpleGraph.lt_extremalNumber_iff, SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_edges, SimpleGraph.Subgraph.incidenceSet_subset_incidenceSet, SimpleGraph.incMatrix_transpose_mul_diag, SimpleGraph.Walk.adj_toSubgraph_iff_mem_edges, Set.sym2_inter, Finset.sym2_insert, SimpleGraph.IsCycles.reachable_deleteEdges, SimpleGraph.Walk.mk_penultimate_end_mem_edges, WellFounded.sym2_gameAdd, SimpleGraph.Walk.mem_support_iff_exists_mem_edges_of_not_nil, Sym2.fromRel_prop, SimpleGraph.isAcyclic_add_edge_iff_of_not_reachable, SimpleGraph.mk'_mem_incidenceSet_left_iff, SimpleGraph.Dart.edge_mem, SimpleGraph.Path.mk'_mem_edges_singleton, QuadraticMap.apply_linearCombination', Finset.sym2_eq_empty, Acc.sym2_gameAdd, SimpleGraph.edgeSet_subset_setOf_not_isDiag, SimpleGraph.Walk.edges_drop, Sym2.card_image_offDiag, Multiset.dedup_sym2, SimpleGraph.Walk.cons_isTrail_iff, SimpleGraph.edgeFinset_subset_edgeFinset, SimpleGraph.EdgeLabeling.get_eq, List.map_mk_sublist_sym2, Finset.coe_sym2, Sym2.map_id, SimpleGraph.Subgraph.incidenceSet_subset, SimpleGraph.Subgraph.edgeSet_coe, SimpleGraph.edgeSet_map, SimpleGraph.lt_extremalNumber_iff_of_nonneg, SimpleGraph.card_incidenceFinset_eq_degree, SimpleGraph.Walk.edges_append, Sym2.IsDiag.not_mem_edgeSet, Sym2.mem_map, Set.mk_mem_sym2_iff, SimpleGraph.edgeFinset_eq_empty, SimpleGraph.disjoint_sdiff_neighborFinset_image, SimpleGraph.regularityReduced_edges_card_aux, SimpleGraph.Walk.edges_injective, SimpleGraph.disjoint_fromEdgeSet, Set.sym2_univ, SimpleGraph.Walk.edgeSet_map, SimpleGraph.Walk.edges_toPath_subset, SimpleGraph.Walk.edges_reverse, QuadraticMap.apply_linearCombination, SimpleGraph.Walk.edgeSet_append, SimpleGraph.degree_le_card_edgeFinset, SimpleGraph.triangle_removal, List.Subperm.sym2, SimpleGraph.Walk.IsSubwalk.edges_subset, Sym2.card_subtype_diag, Sym2.irreflexive_iff_fromRel_subset_diagSet_compl, SimpleGraph.card_edgeFinset_turanGraph, Finset.sum_sym2_filter_not_isDiag, SimpleGraph.lineGraph_adj_iff_exists, SimpleGraph.edgeSet_univ_card, SimpleGraph.Walk.count_edges_takeUntil_le_one, SimpleGraph.card_edgeFinset_induce_support, SimpleGraph.card_edgeFinset_completeEquipartiteGraph, SimpleGraph.Walk.IsTrail.length_le_card_edgeFinset, Disjoint.edgeSet, SimpleGraph.Walk.edgeSet_cons, SimpleGraph.edgeFinset_sup_edge, SimpleGraph.edgeSet_sup, SimpleGraph.Embedding.mapEdgeSet_apply, SimpleGraph.Walk.getLast_edges_eq_mk_penultimate_end, SimpleGraph.fromEdgeSet_union, Sym2.instSubsingleton, QuadraticMap.map_sum, SimpleGraph.Walk.IsSubwalk.edges_isInfix, Sym2.fromRel_proj_prop, SimpleGraph.Walk.coe_edges_toFinset, SimpleGraph.card_toFinset_mem_edgeFinset, Sym2.two_mul_card_image_offDiag, Set.sym2_empty, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, Sym2.mem_diagSet, SimpleGraph.Walk.IsTrail.disjoint_edges_takeUntil_dropUntil, SimpleGraph.Walk.IsEulerian.mem_edges_iff, SimpleGraph.Iso.mapEdgeSet_apply, SimpleGraph.edgeSet_replaceVertex_of_not_adj, SimpleGraph.edgeSet_eq_empty, SimpleGraph.mk'_mem_incidenceSet_iff, SimpleGraph.edgeSet_deleteEdges, Finsupp.sym2Mul_apply_mk, Finset.sym2_val, SimpleGraph.CliqueFree.card_edgeFinset_le, SimpleGraph.Walk.isTrail_cons, SimpleGraph.Walk.edges_map, SimpleGraph.card_edgeSet, Sym2.card, Sym2.pmap_pmap, List.dedup_sym2, SimpleGraph.edgeSet_injective, List.mem_sym2_iff, SimpleGraph.edgeSet_sdiff, List.sym2_eq_sym_two, SimpleGraph.killCopies_def, Sym2.IsDiag.mem_range_diag, Finset.strictMono_sym2, SimpleGraph.edgeSet_subset_compl_diagSet, Sym2.fromRel_mono, SimpleGraph.mem_edgeSet, SimpleGraph.incMatrix_apply, Multiset.sym2_map, SimpleGraph.Subgraph.deleteEdges_deleteEdges, Finset.sym2_image, SimpleGraph.Walk.mem_edges_toSubgraph, SimpleGraph.card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph, SimpleGraph.card_edgeFinset_induce_of_support_subset, SimpleGraph.Walk.mk_start_snd_mem_edges, SimpleGraph.edgeFinset_deleteEdges, Set.mk_preimage_sym2, SimpleGraph.deleteEdges_sdiff_eq_of_le, SimpleGraph.deleteEdges_eq_self, Finsupp.mem_sym2_support_of_mul_ne_zero, SimpleGraph.incidence_other_neighbor_edge, SimpleGraph.adj_iff_exists_edge, SimpleGraph.edgeFinset_inf, Sym2.out_snd_mem, SimpleGraph.incidenceSet_subset, SimpleGraph.EdgeLabeling.labelGraph_adj, SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem, List.mem_sym2_cons_iff, Sym2.fromRel_top_iff, SimpleGraph.map_edgeFinset_induce, SimpleGraph.deleteEdges_deleteEdges, Set.sym2_singleton, SimpleGraph.mk'_mem_incidenceSet_right_iff, SimpleGraph.edgeFinset_card, SimpleGraph.Walk.length_edges, Sym2.diagSet_eq_univ_of_subsingleton, SimpleGraph.Subgraph.edgeSet_inf, SimpleGraph.Iso.mapEdgeSet_symm_apply, SimpleGraph.Walk.mem_support_iff_exists_mem_edges, Sym2.mem_diagSet_iff_eq, Multiset.monotone_sym2, List.sym2_eq_nil_iff, Finset.sym2_eq_image, Multiset.sym2_coe, Sym2.mem_diagSet_iff_isDiag, SimpleGraph.Walk.edges_eq_nil, SimpleGraph.incMatrix_apply_eq_zero_iff, SimpleGraph.mul_card_edgeFinset_turanGraph_le, SimpleGraph.Subgraph.coe_deleteEdges_eq, SimpleGraph.IsTree.card_edgeFinset, Multiset.card_sym2, Finset.sym2_singleton, SimpleGraph.edgeSet_singletonSubgraph, SimpleGraph.incMatrix_mul_transpose_apply_of_adj, Sym2.mem_iff_mem, SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges, SimpleGraph.edgeFinset_ssubset_edgeFinset, Finsupp.sym2_support_eq_preimage_support_mul, SimpleGraph.card_edgeFinset_induce_compl_singleton
«termS(_,_)» 📖» "API Documentation")	CompOp	—

---

← Back to Index