Lp Extension Input Cast

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Euclidean.lpExtensionInput_mp_T {p : ENNReal} {C D : ℝ} (hCD : C = D) (h : LpExtensionInput p C) (e : LpExtensionInput p C = LpExtensionInput p D) : (e.mp h).T = h.T

Transporting an LpExtensionInput along an equality of its constant does not change its operator.