CardEmbedding

Statistics

Metric	Count
Definitions	0
Theorems `card_embedding_eq`, `card_embedding_eq_of_infinite`, `card_embedding_eq_of_unique`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`card_embedding_eq` 📖	mathematical	—	`card` `Function.Embedding` `Nat.descFactorial`	—	`subsingleton` `induction_empty_option` `card_congr` `card_pempty` `Nat.descFactorial_zero` `card_eq_one_iff` `PEmpty.instIsEmpty` `DFunLike.ext` `card_option` `Nat.descFactorial_succ` `card_sigma` `Finset.sum_congr` `card_compl_set` `card_range` `Function.instEmbeddingLikeEmbedding` `Finset.sum_const` `mul_comm`
`card_embedding_eq_of_infinite` 📖	mathematical	—	`card` `Function.Embedding`	—	`card_eq_zero` `Function.Embedding.is_empty`
`card_embedding_eq_of_unique` 📖	mathematical	—	`card` `Function.Embedding`	—	`card_congr`

---