NCard

Statistics

Metric	Count
Definitions	0
Theorems `measurable_encard`, `measurable_ncard`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable_encard` 📖	mathematical	—	`Measurable` `Set` `ENat` `Set.instMeasurableSpace` `ENat.instMeasurableSpace` `Set.encard`	—	`ENat.measurable_iff` `Set.Countable.measurableSet` `Set.instMeasurableSingletonClass` `Set.Countable.mono` `Set.finite_of_encard_eq_coe` `Set.Countable.setOf_finite`
`measurable_ncard` 📖	mathematical	—	`Measurable` `Set` `Set.instMeasurableSpace` `Nat.instMeasurableSpace` `Set.ncard`	—	`Measurable.comp` `Measurable.of_discrete` `ENat.instDiscreteMeasurableSpace` `measurable_encard`

---