Introduction to Measure Theory, Section 1.2.3: Non-measurable sets

A companion to (the introduction to) Section 1.2.3 of the book "An introduction to Measure Theory".

theorem LebesgueMeasurable.nonmeasurable : ∃ E ⊆ ⇑Real.equiv_EuclideanSpace' '' Set.Icc 0 1, ¬LebesgueMeasurable E

Proposition 1.2.18