English
If hs and ht are UniqueDiffWithinAt for s and t respectively, then their product s × t has UniqueDiffWithinAt at (x,y).
Русский
Если s и t имеют уникальную дифференцируемость в точках x и y, соответственно, то их произведение имеет уникальную дифференцируемость в точке (x,y).
LaTeX
$$$ (\\text{hs}) \\land (\\text{ht}) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s \\times t)(x,y) $$$
Lean4
/-- The product of two sets of unique differentiability at points `x` and `y` has unique
differentiability at `(x, y)`. -/
theorem prod {t : Set F} {y : F} (hs : UniqueDiffWithinAt 𝕜 s x) (ht : UniqueDiffWithinAt 𝕜 t y) :
UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y) :=
by
rw [uniqueDiffWithinAt_iff] at hs ht ⊢
rw [closure_prod_eq]
refine ⟨?_, hs.2, ht.2⟩
have : _ ≤ Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)) :=
Submodule.span_mono (union_subset (subset_tangentConeAt_prod_left ht.2) (subset_tangentConeAt_prod_right hs.2))
rw [LinearMap.span_inl_union_inr, SetLike.le_def] at this
exact (hs.1.prod ht.1).mono this
