prod — Mathlib

English

The product of two sets with UniqueDiffOn has UniqueDiffOn.

Русский

Произведение двух множеств с уникальной дифференцируемостью также обладает этой свойством.

LaTeX

$$$ \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s) \\land \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(t) \\Rightarrow \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s \\times t) $$$

Lean4

/-- The product of two sets of unique differentiability is a set of unique differentiability. -/
theorem prod {t : Set F} (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) : UniqueDiffOn 𝕜 (s ×ˢ t) := fun ⟨x, y⟩ h =>
  UniqueDiffWithinAt.prod (hs x h.1) (ht y h.2)

Похожие утверждения