univ_pi — Mathlib

English

For a finite index set ι and families E_i with each coordinate having UniqueDiffWithinAt, the product over i of s_i has UniqueDiffWithinAt on the product space.

Русский

Если индексовое множество ι конечно и в каждой координате s_i есть уникальная дифференцируемость, то произведение по i множества s_i обладает уникальной дифференцируемостью на произведённом пространстве.

LaTeX

$$$ (\\forall i, \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s_i,x_i)) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(\\mathrm{Set.univ.pi}\\n s)\\; x $$$

Lean4

theorem univ_pi (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
    (s : ∀ i, Set (E i)) (x : ∀ i, E i) (h : ∀ i, UniqueDiffWithinAt 𝕜 (s i) (x i)) :
    UniqueDiffWithinAt 𝕜 (Set.pi univ s) x := by
  classical
  simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
  refine ⟨(dense_pi univ fun i _ => (h i).1).mono ?_, fun i _ => (h i).2⟩
  norm_cast
  simp only [← Submodule.iSup_map_single, iSup_le_iff, LinearMap.map_span, Submodule.span_le, ← mapsTo_iff_image_subset]
  exact fun i => (mapsTo_tangentConeAt_pi fun j _ => (h j).2).mono Subset.rfl Submodule.subset_span

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