Commit 2024-01-28 15:34 9f35a083
View on Github →feat: add lemmas nullMeasurableSet_lt' and nullMeasurableSet_le (#10074)
Prior to this commit the state of Mathlib was:
import Mathlib
#check measurableSet_lt -- Exists
#check measurableSet_lt' -- Exists
#check measurableSet_le -- Exists
#check nullMeasurableSet_lt -- Exists
#check nullMeasurableSet_lt' -- Missing
#check nullMeasurableSet_le -- Missing