Tsupport Product

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

theorem CKN.tsupport_mul_prod_eq {X : Type u_1} {Y : Type u_2} {M : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [MulZeroClass M] [NoZeroDivisors M] (ψ : X → M) (θ : Y → M) : (tsupport fun (z : X × Y) => ψ z.1 * θ z.2) = tsupport ψ ×ˢ tsupport θ

The topological support of a separated product ψ(x) θ(y) on a product space is the product of the two topological supports.