Commit 2024-08-30 13:02 5c93cb82

feat(Set,MeasurableSpace): lemmas about {s | s.Finite} (#16195) For a countable type α,

• {s : Set α | s.Finite} is countable, hence measurable;
• {s : Set α | s.Infinite} is measurable.