prod — Mathlib

English

A second instance of product stability: if hs and ht hold, then for the product space the MDiff property holds.

Русский

Дополнительное свойство стабильности для произведения пространств: если для s и t выполняются условия, то для произведения выполняется MDiff.

LaTeX

$$UniqueMDiffWithinAt I s → UniqueMDiffWithinAt I' t → UniqueMDiffWithinAt (I.prod I') (Set.instSProd.sprod s t) { fst := x, snd := y }$$

Lean4

nonrec theorem prod {x : M} {y : M'} {s t} (hs : UniqueMDiffWithinAt I s x) (ht : UniqueMDiffWithinAt I' t y) :
    UniqueMDiffWithinAt (I.prod I') (s ×ˢ t) (x, y) :=
  by
  refine (hs.prod ht).mono ?_
  rw [ModelWithCorners.range_prod, ← prod_inter_prod]
  rfl

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