uniqueDiffOn_Ici — Mathlib

English

The finite universal pi-product preserves UniqueDiffOn; i.e., if each s_i has UniqueDiffOn, then Set.univ.pi s has UniqueDiffOn.

Русский

Сохранение уникальной дифференцируемости в конечном универсальном пи-произведении: если каждый s_i имеет UniqueDiffOn, то Set.univ.pi s имеет UniqueDiffOn.

LaTeX

$$$ (\\forall i, \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s_i)) \\Rightarrow \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(\\mathrm{Set.univ.pi}\\, s) $$$

Lean4

theorem uniqueDiffOn_Ici (a : ℝ) : UniqueDiffOn ℝ (Ici a) :=
  uniqueDiffOn_convex (convex_Ici a) <| by simp only [interior_Ici, nonempty_Ioi]

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