proximity_coe_eq_proximity_sub_const_zero

English

For finite a0, proximity f a0 equals proximity (f − a0) 0; i.e., shifting by a finite value reduces to evaluating proximity at zero for the shifted function.

Русский

Для конечного a0 proximity f a0 равно proximity (f − a0) 0; то есть сдвиг на конечное значение эквивалентен вычислению близости в нуле для функции, смещенной на a0.

LaTeX

$$$\mathrm{proximity}(f,a_0) = \mathrm{proximity}(f - (\lambda\mapsto a_0),0) \quad (a_0 \text{ finite})$$$

Lean4

/-- For finite values `a₀`, the proximity function `proximity f a₀` equals the proximity function for
the value zero of the shifted function `f - a₀`.
-/
theorem proximity_coe_eq_proximity_sub_const_zero : proximity f a₀ = proximity (f - fun _ ↦ a₀) 0 := by simp [proximity]

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