snd

Mathlib.Analysis.Calculus.ContDiff.Basic

URI: https://scilib.ai/kg/mathlib#ContDiff.snd

← MathLib Explorer

English

At a fixed point x in E × F, the map p ↦ p.1 is ContDiff At x.

Русский

В точке x в произведении карта p ↦ p.1 является ContDiffAt.

LaTeX

$$$\forall p,\; \ContDiffAt 𝕜 n (\mathrm{Prod.fst}) p$$$

Lean4

/-- Postcomposing `f` with `Prod.snd` is `C^n` -/
@[fun_prop]
theorem snd {f : E → F × G} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun x => (f x).2 :=
  contDiff_snd.comp hf

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru