Uniqueness of weak partial derivatives

Locally integrable weak partial derivatives of the same function on an open set agree almost everywhere.

theorem CKN.hasWeakPartialDerivOn_unique_ae {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {i : Fin d} {f g h : Vec d → ℝ} (hgLoc : MeasureTheory.LocallyIntegrableOn g U MeasureTheory.volume) (hhLoc : MeasureTheory.LocallyIntegrableOn h U MeasureTheory.volume) (hg : HasWeakPartialDerivOn U i f g) (hh : HasWeakPartialDerivOn U i f h) : g =ᵐ[MeasureTheory.volume.restrict U] h

Locally integrable weak partial derivatives of the same function agree almost everywhere.