Theorem MeasurableSpace.forall_generateFrom_mem_iff_mem_iff

Modification history

2023-07-08 15:27
Mathlib/MeasureTheory/MeasurableSpaceDef.lean
feat: define `HasCountableSeparatingOn` (#5675) …
Added MeasurableSpace.forall_generateFrom_mem_iff_mem_iffView on Github →