Sym

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

Statistics

Metric	Count
Definitions sym, sym2, symInsertEquiv, instFintype	4
Theorems sym, sym2, card_sym2, coe_sym2, diag_mem_sym2_iff, diag_mem_sym2_mem_iff, eq_empty_of_sym_eq_empty, image_diag_union_image_offDiag, injective_sym2, isDiag_mk_of_mem_diag, mem_sym2_iff, mem_sym_iff, mk_mem_sym2_iff, monotone_sym2, not_isDiag_mk_of_mem_offDiag, replicate_mem_sym, strictMono_sym2, sym2_cons, sym2_empty, sym2_eq_empty, sym2_eq_image, sym2_image, sym2_insert, sym2_map, sym2_mono, sym2_nonempty, sym2_singleton, sym2_toFinset, sym2_univ, sym2_val, symInsertEquiv_apply_fst, symInsertEquiv_apply_snd_coe, symInsertEquiv_symm_apply_coe, sym_empty, sym_eq_empty, sym_fill_mem, sym_filterNe_mem, sym_inter, sym_mono, sym_nonempty, sym_singleton, sym_succ, sym_union, sym_univ, sym_zero	45
Total	49

Finset

Definitions

Name	Category	Theorems
sym 📖	CompOp	23 math math: sym_univ, mem_sym_iff, sym_nonempty, map_sym_eq_piAntidiag, DividedPowers.dpow_sum', Nonempty.sym, replicate_mem_sym, sym_union, norm_iteratedFDerivWithin_prod_le, DividedPowers.dpow_sum, sum_pow_of_commute, sym_inter, sym_zero, sym_singleton, sym_eq_empty, norm_iteratedFDeriv_prod_le, symInsertEquiv_apply_snd_coe, symInsertEquiv_apply_fst, sym_empty, symInsertEquiv_symm_apply_coe, sym_succ, sum_pow, sym_mono
sym2 📖	CompOp	37 math math: mk_mem_sym2_iff, SimpleGraph.edgeFinset_subset_sym2_of_support_subset, sym2_toFinset, QuadraticMap.map_finsuppSum, card_sym2, mem_sym2_iff, sym2_mono, sym2_map, Finsupp.support_sym2Mul_subset, sym2_empty, QuadraticMap.map_finsuppSum', SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton, sym2_nonempty, sym2_cons, Nonempty.sym2, sym2_univ, injective_sym2, diag_mem_sym2_iff, QuadraticMap.map_sum', SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton, image_diag_union_image_offDiag, monotone_sym2, sym2_insert, sym2_eq_empty, coe_sym2, QuadraticMap.apply_linearCombination, sum_sym2_filter_not_isDiag, QuadraticMap.map_sum, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, sym2_val, strictMono_sym2, sym2_image, Finsupp.mem_sym2_support_of_mul_ne_zero, SimpleGraph.map_edgeFinset_induce, sym2_eq_image, sym2_singleton, Finsupp.sym2_support_eq_preimage_support_mul
symInsertEquiv 📖	CompOp	3 math math: symInsertEquiv_apply_snd_coe, symInsertEquiv_apply_fst, symInsertEquiv_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_sym2 📖	mathematical	—	card Sym2 sym2 Nat.choose	—	card_def sym2_val Multiset.card_sym2
coe_sym2 📖	mathematical	—	SetLike.coe Finset Sym2 instSetLike sym2 Set.sym2	—	Set.ext Sym2.ind
diag_mem_sym2_iff 📖	mathematical	—	Sym2 Finset instMembership sym2 Sym2.diag	—	—
diag_mem_sym2_mem_iff 📖	mathematical	—	Finset instMembership	—	mem_sym2_iff mk_mem_sym2_iff
eq_empty_of_sym_eq_empty 📖	—	sym Finset Sym instEmptyCollection	—	—	Mathlib.Tactic.Contrapose.contrapose₁ Nonempty.sym
image_diag_union_image_offDiag 📖	mathematical	—	Finset Sym2 instUnion Sym2.instDecidableEq image diag offDiag sym2	—	image_union diag_union_offDiag sym2_eq_image
injective_sym2 📖	mathematical	—	Finset Sym2 sym2	—	ext
isDiag_mk_of_mem_diag 📖	mathematical	Finset instMembership diag	Sym2.IsDiag	—	—
mem_sym2_iff 📖	mathematical	—	Sym2 Finset instMembership sym2	—	nodup sym2_val Multiset.mem_sym2_iff
mem_sym_iff 📖	mathematical	—	Sym Finset instMembership sym	—	mem_singleton notMem_empty Sym.eq_nil_of_card_zero mem_sup mem_image Sym.mem_cons Sym.exists_eq_cons_of_succ Sym.mem_cons_self mem_image_of_mem Sym.mem_cons_of_mem
mk_mem_sym2_iff 📖	mathematical	—	Sym2 Finset instMembership sym2	—	nodup sym2_val Multiset.mk_mem_sym2_iff
monotone_sym2 📖	mathematical	—	Monotone Finset Sym2 PartialOrder.toPreorder partialOrder sym2	—	sym2_mono
not_isDiag_mk_of_mem_offDiag 📖	mathematical	Finset instMembership offDiag	Sym2.IsDiag	—	—
replicate_mem_sym 📖	mathematical	Finset instMembership	Sym sym Sym.replicate	—	mem_sym_iff Sym.mem_replicate
strictMono_sym2 📖	mathematical	—	StrictMono Finset Sym2 PartialOrder.toPreorder partialOrder sym2	—	Monotone.strictMono_of_injective monotone_sym2 injective_sym2
sym2_cons 📖	mathematical	Finset instMembership	sym2 cons disjUnion Sym2 map Sym2.mkEmbedding	—	val_injective Multiset.sym2_cons
sym2_empty 📖	mathematical	—	sym2 Finset instEmptyCollection Sym2	—	—
sym2_eq_empty 📖	mathematical	—	sym2 Finset Sym2 instEmptyCollection	—	val_eq_zero sym2_val Multiset.sym2_eq_zero_iff
sym2_eq_image 📖	mathematical	—	sym2 image Sym2 Sym2.instDecidableEq SProd.sprod Finset instSProd	—	ext
sym2_image 📖	mathematical	—	sym2 image Sym2 Sym2.instDecidableEq Sym2.map	—	val_injective Multiset.dedup_sym2 Multiset.sym2_map
sym2_insert 📖	mathematical	—	sym2 Finset instInsert Sym2 instUnion Sym2.instDecidableEq image	—	insert_eq_of_mem image_insert insert_union cons_eq_insert map_eq_image disjUnion.congr_simp disjUnion_eq_union sym2_cons
sym2_map 📖	mathematical	—	sym2 map Sym2 Function.Embedding.sym2Map	—	val_injective Multiset.sym2_map
sym2_mono 📖	mathematical	Finset instHasSubset	Sym2 sym2	—	—
sym2_nonempty 📖	mathematical	—	Nonempty Sym2 sym2	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ sym2_eq_empty
sym2_singleton 📖	mathematical	—	sym2 Finset instSingleton Sym2 Sym2.diag	—	—
sym2_toFinset 📖	mathematical	—	sym2 Multiset.toFinset Sym2 Sym2.instDecidableEq Multiset.sym2	—	ext Sym2.ind
sym2_univ 📖	mathematical	—	sym2 univ Sym2	—	ext
sym2_val 📖	mathematical	—	val Sym2 sym2 Multiset.sym2	—	—
symInsertEquiv_apply_fst 📖	mathematical	Finset instMembership	Sym SetLike.instMembership instSetLike sym DFunLike.coe Equiv instInsert EquivLike.toFunLike Equiv.instEquivLike symInsertEquiv Sym.filterNe	—	—
symInsertEquiv_apply_snd_coe 📖	mathematical	Finset instMembership	Sym Sym.filterNe SetLike.instMembership instSetLike sym instInsert DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike symInsertEquiv	—	—
symInsertEquiv_symm_apply_coe 📖	mathematical	Finset instMembership	Sym SetLike.instMembership instSetLike sym instInsert DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm symInsertEquiv Sym.fill	—	—
sym_empty 📖	mathematical	—	sym Finset instEmptyCollection Sym	—	—
sym_eq_empty 📖	mathematical	—	sym Finset Sym instEmptyCollection	—	singleton_ne_empty eq_empty_of_sym_eq_empty sym_empty
sym_fill_mem 📖	mathematical	Sym Finset instMembership sym	instInsert Sym.fill	—	mem_sym_iff mem_insert Sym.mem_fill_iff
sym_filterNe_mem 📖	mathematical	Sym Finset instMembership sym	Sym.filterNe erase	—	mem_sym_iff mem_erase Multiset.mem_filter
sym_inter 📖	mathematical	—	sym Finset instInter Sym instDecidableEqSym	—	ext
sym_mono 📖	mathematical	Finset instHasSubset	Sym sym	—	mem_sym_iff
sym_nonempty 📖	mathematical	—	Nonempty Sym sym	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ sym_eq_empty
sym_singleton 📖	mathematical	—	sym Finset instSingleton Sym Sym.replicate	—	eq_singleton_iff_unique_mem replicate_mem_sym mem_singleton Sym.eq_replicate_iff eq_of_mem_singleton mem_sym_iff
sym_succ 📖	mathematical	—	sym sup Finset Sym Lattice.toSemilatticeSup instLattice instDecidableEqSym instOrderBot image Sym.cons	—	—
sym_union 📖	mathematical	—	Finset Sym instHasSubset instUnion instDecidableEqSym sym	—	union_subset sym_mono subset_union_left subset_union_right
sym_univ 📖	mathematical	—	sym univ Sym instFintypeSymOfDecidableEq	—	eq_univ_iff_forall mem_sym_iff mem_univ
sym_zero 📖	mathematical	—	sym Sym Finset instSingleton Sym.instEmptyCollectionOfNatNat	—	—

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sym 📖	mathematical	Finset.Nonempty	Sym Finset.sym	—	Finset.replicate_mem_sym
sym2 📖	mathematical	Finset.Nonempty	Sym2 Finset.sym2	—	Finset.sym2_nonempty

Sym2

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	54 math math: SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le, SimpleGraph.edgeFinset_subset_sym2_of_support_subset, SimpleGraph.two_mul_card_edgeFinset, SimpleGraph.sum_degrees_eq_twice_card_edges, card_subtype_not_diag, SimpleGraph.card_edgeFinset_sup_edge, SimpleGraph.edgeFinset_top, SimpleGraph.map_edgeFinset_induce_of_support_subset, SimpleGraph.extremalNumber_le_iff_of_nonneg, SimpleGraph.card_edgeFinset_map, SimpleGraph.farFromTriangleFree_iff, SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff, SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges, SimpleGraph.edgeFinset_map, SimpleGraph.card_edgeFinset_of_isExtremal_free, SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges', SimpleGraph.edgeFinset_replaceVertex_of_adj, SimpleGraph.LocallyLinear.card_edgeFinset, SimpleGraph.card_edgeFinset_le_extremalNumber, SimpleGraph.farFromTriangleFree.le_card_sub_card, SimpleGraph.isExtremal_free_iff, SimpleGraph.card_edgeFinset_turanGraph_add, SimpleGraph.edgeFinset_replaceVertex_of_not_adj, SimpleGraph.extremalNumber_top, SimpleGraph.card_edgeFinset_deleteIncidenceSet_le_extremalNumber, SimpleGraph.card_edgeFinset_top_eq_card_choose_two, SimpleGraph.dart_card_eq_twice_card_edges, SimpleGraph.extremalNumber_of_fintypeCard_eq, SimpleGraph.edgeFinset_deleteIncidenceSet_eq_filter, SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj, card_diagSet_compl, SimpleGraph.card_edgeFinset_replaceVertex_of_adj, SimpleGraph.sum_degrees_support_eq_twice_card_edges, SimpleGraph.extremalNumber_le_iff, SimpleGraph.card_edgeFinset_deleteIncidenceSet, SimpleGraph.lt_extremalNumber_iff, SimpleGraph.lt_extremalNumber_iff_of_nonneg, SimpleGraph.disjoint_sdiff_neighborFinset_image, SimpleGraph.regularityReduced_edges_card_aux, SimpleGraph.triangle_removal, card_subtype_diag, SimpleGraph.card_edgeFinset_turanGraph, SimpleGraph.card_edgeFinset_induce_support, SimpleGraph.card_edgeFinset_completeEquipartiteGraph, SimpleGraph.edgeFinset_sup_edge, SimpleGraph.CliqueFree.card_edgeFinset_le, card, SimpleGraph.card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph, SimpleGraph.card_edgeFinset_induce_of_support_subset, SimpleGraph.map_edgeFinset_induce, SimpleGraph.card_topEdgeLabeling, SimpleGraph.mul_card_edgeFinset_turanGraph_le, SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges, SimpleGraph.card_edgeFinset_induce_compl_singleton

---

← Back to Index