const — Mathlib

English

A constant function has temperate growth since all derivatives vanish and the bound holds with k = 0 and C = ‖c‖.

Русский

Постоянная функция имеет темперированный рост, так как все производные нули, граница выполняется со значениями k = 0 и C = ‖c‖.

LaTeX

$$$\\forall c\\in F: \\text{HasTemperateGrowth}(x\\mapsto c).$$$

Lean4

theorem _root_.Function.HasTemperateGrowth.const (c : F) : Function.HasTemperateGrowth (fun _ : E ↦ c) :=
  .of_fderiv (by simpa using .zero) (differentiable_const c) (k := 0) (C := ‖c‖) (fun x ↦ by simp)

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