NatCount

Statistics

Metric	Count
Definitions	0
Theorems `count_le_cardinal`, `count_le_setENCard`, `count_le_setNCard`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`count_le_cardinal` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.instNatCast` `count` `Set.Elem` `setOf`	—	`count_eq_card_fintype` `Cardinal.mk_fintype` `Cardinal.mk_subtype_mono`
`count_le_setENCard` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `count` `Set.encard` `setOf`	—	`count_le_cardinal`
`count_le_setNCard` 📖	mathematical	—	`count` `Set.ncard` `setOf`	—	`Set.ncard_def` `ENat.coe_le_coe` `ENat.coe_toNat` `count_le_setENCard`

---