Nat

Statistics

Metric	Count
Definitions	0
Theorems `ncard_Icc_nat`, `ncard_Ico_nat`, `ncard_Iic_nat`, `ncard_Iio_nat`, `ncard_Ioc_nat`, `ncard_Ioo_nat`, `ncard_uIcc_nat`	7
Total	7

Name	Kind	Assumes	Proves	Validates	Depends On
`ncard_Icc_nat` 📖	mathematical	—	`ncard` `Icc` `Nat.instPreorder`	—	`Finset.coe_Icc` `Nat.card_Icc`
`ncard_Ico_nat` 📖	mathematical	—	`ncard` `Ico` `Nat.instPreorder`	—	`Finset.coe_Ico` `Nat.card_Ico`
`ncard_Iic_nat` 📖	mathematical	—	`ncard` `Iic` `Nat.instPreorder`	—	`Finset.coe_Iic` `Nat.card_Iic`
`ncard_Iio_nat` 📖	mathematical	—	`ncard` `Iio` `Nat.instPreorder`	—	`Finset.coe_Iio` `Nat.card_Iio`
`ncard_Ioc_nat` 📖	mathematical	—	`ncard` `Ioc` `Nat.instPreorder`	—	`Finset.coe_Ioc` `Nat.card_Ioc`
`ncard_Ioo_nat` 📖	mathematical	—	`ncard` `Ioo` `Nat.instPreorder`	—	`Finset.coe_Ioo` `Nat.card_Ioo`
`ncard_uIcc_nat` 📖	mathematical	—	`ncard` `uIcc` `DistribLattice.toLattice` `instDistribLatticeNat`	—	`Finset.coe_uIcc` `Nat.card_uIcc`

---