Planar area of coordinate lines and graphs

Coordinate lines and continuous graphs over compact intervals have zero planar Lebesgue measure. Interchanging the real and imaginary coordinates preserves planar area.

theorem Complex.volume_setOf_re_eq (c : ℝ) : MeasureTheory.volume {z : ℂ | z.re = c} = 0

A vertical coordinate line has zero planar area.

theorem Complex.volume_setOf_im_eq (c : ℝ) : MeasureTheory.volume {z : ℂ | z.im = c} = 0

A horizontal coordinate line has zero planar area.

theorem Complex.volume_setOf_re_mem_Icc_im_eq {a b : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : MeasureTheory.volume {z : ℂ | z.re ∈ Set.Icc a b ∧ z.im = f z.re} = 0

A continuous graph over a compact interval has zero planar area.

theorem Complex.measurePreserving_coordinateSwapCLE : MeasureTheory.MeasurePreserving (⇑coordinateSwapCLE) MeasureTheory.volume MeasureTheory.volume

Interchanging the coordinates preserves planar area.