div_const

Mathlib.Geometry.Manifold.Algebra.Monoid

URI: https://scilib.ai/kg/mathlib#ContMDiffAt.div_const

English

If hf is ContMDiffWithinAt for f at x, then f/c is ContMDiffWithinAt at x.

Русский

Если hf — ContMDiffWithinAt для f в точке x, то f/c — ContMDiffWithinAt в этой точке.

LaTeX

$$$(hf : ContMDiffWithinAt I' I n f s x) \to \ ContMDiffWithinAt I' I n (\lambda x, f(x)/c) s x$$$

Lean4

@[to_additive]
nonrec theorem div_const (hf : ContMDiffAt I' I n f x) : ContMDiffAt I' I n (fun x ↦ f x / c) x :=
  hf.div_const c

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

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

Разделы

Аффилиация

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