Antidiagonal

Statistics

Metric	Count
Definitions	0
Theorems `antidiagonal_coe`, `antidiagonal_coe'`, `antidiagonal_cons`, `antidiagonal_eq_map_powerset`, `antidiagonal_map_fst`, `antidiagonal_map_snd`, `antidiagonal_zero`, `card_antidiagonal`, `mem_antidiagonal`	9
Total	9

Name	Kind	Assumes	Proves	Validates	Depends On
`antidiagonal_coe` 📖	mathematical	—	`antidiagonal` `ofList` `Multiset` `powersetAux`	—	—
`antidiagonal_coe'` 📖	mathematical	—	`antidiagonal` `ofList` `Multiset` `powersetAux'`	—	`revzip_powersetAux_perm_aux'`
`antidiagonal_cons` 📖	mathematical	—	`antidiagonal` `cons` `Multiset` `instAdd` `map`	—	`antidiagonal_coe'` `powersetAux'_cons` `map_congr`
`antidiagonal_eq_map_powerset` 📖	mathematical	—	`antidiagonal` `map` `Multiset` `instSub` `powerset`	—	`induction_on` `map_congr` `zero_sub` `antidiagonal_cons` `powerset_cons` `map_add` `map_map` `sub_cons` `erase_cons_head` `add_comm` `cons_sub_of_le` `mem_powerset`
`antidiagonal_map_fst` 📖	mathematical	—	`map` `Multiset` `antidiagonal` `powerset`	—	`map_congr` `antidiagonal_coe'` `List.revzip_map_fst` `powerset_coe'`
`antidiagonal_map_snd` 📖	mathematical	—	`map` `Multiset` `antidiagonal` `powerset`	—	`map_congr` `antidiagonal_coe'` `List.revzip_map_snd` `coe_reverse` `powerset_coe'`
`antidiagonal_zero` 📖	mathematical	—	`antidiagonal` `Multiset` `instZero` `instSingleton`	—	—
`card_antidiagonal` 📖	mathematical	—	`card` `Multiset` `antidiagonal` `Monoid.toNatPow` `Nat.instMonoid`	—	`card_powerset` `card_map` `antidiagonal_map_fst`
`mem_antidiagonal` 📖	mathematical	—	`Multiset` `instMembership` `antidiagonal` `instAdd`	—	`revzip_powersetAux` `revzip_powersetAux_lemma` `le_add_right` `add_tsub_cancel_left` `instOrderedSub` `instAddLeftReflectLE`

---