div_const — Mathlib

English

If hf is ContMDiffWithinAt for f, then f/c is ContMDiffWithinAt (division by a constant).

Русский

Если hf — ContMDiffWithinAt для f, то f/c — ContMDiffWithinAt (деление на константу).

LaTeX

$$$\text{ContMDiffWithinAt } I' I n f s x \Rightarrow \text{ContMDiffWithinAt } I' I n (\lambda x, f(x)/c) s x$$$

Lean4

@[to_additive]
theorem div_const (hf : ContMDiffWithinAt I' I n f s x) : ContMDiffWithinAt I' I n (fun x ↦ f x / c) s x := by
  simpa only [div_eq_mul_inv] using hf.mul contMDiffWithinAt_const

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