Theorem MeasurableSet.setOf_infinite

Modification history

2026-07-17 09:57
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
chore(Data): rename `setOf` to `Set.ofPred` (#41507) …
Deleted MeasurableSet.setOf_infiniteView on Github →
2025-11-28 16:39
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
feat(MeasureTheory): subsetness is measurable (#32096)
Modified MeasurableSet.setOf_infiniteView on Github →
2025-04-03 10:57
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
chore: split `MeasureTheory.MeasurableSpace.Basic` (#23523) …
Modified MeasurableSet.setOf_infiniteView on Github →
2024-08-30 13:02
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
feat(Set,MeasurableSpace): lemmas about `{s | s.Finite}` (#16195) …
Added MeasurableSet.setOf_infiniteView on Github →