Sym

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

Statistics

Metric	Count
Definitions `sym`, `sym2`	2
Theorems `sym`, `sym2`, `sym2`, `sym`, `sym2`, `sym2`, `dedup_sym2`, `first_mem_of_cons_mem_sym`, `left_mem_of_mk_mem_sym2`, `length_sym`, `length_sym2`, `map_mk_disjoint_sym2`, `map_mk_sublist_sym2`, `mem_of_mem_of_mem_sym`, `mem_sym2_cons_iff`, `mem_sym2_iff`, `mk_mem_sym2`, `mk_mem_sym2_iff`, `right_mem_of_mk_mem_sym2`, `setOf_mem_sym2`, `sym2_eq_nil_iff`, `sym2_eq_sym_two`, `sym2_map`, `sym_map`, `sym_one_eq`, `sym_sublist_sym_cons`	26
Total	28

List

Definitions

Name	Category	Theorems
`sym` 📖	CompOp	7 math math: `Sublist.sym`, `sym_map`, `length_sym`, `sym_sublist_sym_cons`, `sym_one_eq`, `Nodup.sym`, `sym2_eq_sym_two`
`sym2` 📖	CompOp	17 math math: `setOf_mem_sym2`, `length_sym2`, `Perm.sym2`, `Sublist.sym2`, `Nodup.sym2`, `mk_mem_sym2`, `sym2_map`, `mk_mem_sym2_iff`, `map_mk_disjoint_sym2`, `map_mk_sublist_sym2`, `Subperm.sym2`, `dedup_sym2`, `mem_sym2_iff`, `sym2_eq_sym_two`, `mem_sym2_cons_iff`, `sym2_eq_nil_iff`, `Multiset.sym2_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup_sym2` 📖	mathematical	—	`dedup` `Sym2` `Sym2.instDecidableEq` `sym2`	—	`dedup_cons_of_mem` `Sym2.eq_swap` `Subset.dedup_append_right` `map_mk_sublist_sym2` `dedup_cons_of_notMem` `sym2.eq_2` `Disjoint.dedup_append` `map_mk_disjoint_sym2` `dedup_map_of_injective` `Function.Embedding.injective`
`first_mem_of_cons_mem_sym` 📖	—	`Sym` `sym` `Sym.cons`	—	—	`mem_of_mem_of_mem_sym` `Sym.mem_cons_self`
`left_mem_of_mk_mem_sym2` 📖	—	`Sym2` `sym2`	—	—	`mem_sym2_cons_iff` `Sym2.eq_iff`
`length_sym` 📖	mathematical	—	`Sym` `sym` `Nat.multichoose`	—	—
`length_sym2` 📖	mathematical	—	`Sym2` `sym2` `Nat.choose`	—	`sym2.eq_2` `Nat.choose_succ_succ` `Nat.choose_one_right`
`map_mk_disjoint_sym2` 📖	mathematical	—	`Sym2` `sym2`	—	—
`map_mk_sublist_sym2` 📖	mathematical	—	`Sym2` `sym2`	—	`Sym2.eq_swap`
`mem_of_mem_of_mem_sym` 📖	—	`Sym` `Sym.instMembership` `sym`	—	—	—
`mem_sym2_cons_iff` 📖	mathematical	—	`Sym2` `sym2`	—	—
`mem_sym2_iff` 📖	mathematical	—	`Sym2` `sym2`	—	`Sym2.ind`
`mk_mem_sym2` 📖	mathematical	—	`Sym2` `sym2`	—	`mem_sym2_cons_iff`
`mk_mem_sym2_iff` 📖	mathematical	—	`Sym2` `sym2`	—	`left_mem_of_mk_mem_sym2` `right_mem_of_mk_mem_sym2` `mk_mem_sym2`
`right_mem_of_mk_mem_sym2` 📖	—	`Sym2` `sym2`	—	—	`left_mem_of_mk_mem_sym2` `Sym2.eq_swap`
`setOf_mem_sym2` 📖	mathematical	—	`setOf` `Sym2` `sym2` `Set.sym2`	—	`Set.ext` `Sym2.ind`
`sym2_eq_nil_iff` 📖	mathematical	—	`sym2` `Sym2`	—	—
`sym2_eq_sym_two` 📖	mathematical	—	`Sym2` `Sym` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Sym2.equivSym` `sym2` `sym`	—	`sym.eq_2` `sym.eq_3` `sym_one_eq` `sym2.eq_2`
`sym2_map` 📖	mathematical	—	`sym2` `Sym2` `Sym2.map`	—	—
`sym_map` 📖	mathematical	—	`sym` `Sym` `Sym.map`	—	—
`sym_one_eq` 📖	mathematical	—	`sym` `Sym` `Sym.cons` `Sym.nil`	—	`sym.eq_2` `sym.eq_3` `sym.eq_1`
`sym_sublist_sym_cons` 📖	mathematical	—	`Sym` `sym`	—	`Sublist.sym`

List.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sym` 📖	mathematical	—	`Sym` `List.sym`	—	—
`sym2` 📖	mathematical	—	`Sym2` `List.sym2`	—	`List.sym2.eq_2` `append` `cons` `map` `of_cons` `List.left_mem_of_mk_mem_sym2`

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sym2` 📖	mathematical	—	`Sym2` `List.sym2`	—	`Sym2.eq_swap` `add_left_comm`

List.Sublist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sym` 📖	mathematical	—	`Sym` `List.sym`	—	—
`sym2` 📖	mathematical	—	`Sym2` `List.sym2`	—	—

List.Subperm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sym2` 📖	mathematical	—	`Sym2` `List.sym2`	—	`List.Perm.sym2` `List.Sublist.sym2`

---

← Back to Index