prod — Mathlib

English

If hs and ht hold for two spaces, then their product space has UniqueMDiffOn.

Русский

Если для двух пространств выполняются условия MDiff, то их произведение имеет MDiffOn.

LaTeX

$$UniqueMDiffOn I s → UniqueMDiffOn I' t → UniqueMDiffOn (I.prod I') (Set.instSProd.sprod s t)$$

Lean4

theorem prod {s : Set M} {t : Set M'} (hs : UniqueMDiffOn I s) (ht : UniqueMDiffOn I' t) :
    UniqueMDiffOn (I.prod I') (s ×ˢ t) := fun x h ↦ (hs x.1 h.1).prod (ht x.2 h.2)

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