mono_set — Mathlib

English

If c ≤ c' and ApproximatesLinearOn f f' s c holds, then it also holds with constant c' on s.

Русский

Если константа c не превосходит c', и ApproximatesLinearOn выполняется на s с c, то она также верна на s с c'.

LaTeX

$$$ c \le c' \Rightarrow \text{ApproximatesLinearOn}(f,f',s,c) \Rightarrow \text{ApproximatesLinearOn}(f,f',s,c') $$$

Lean4

theorem mono_set (hst : s ⊆ t) (hf : ApproximatesLinearOn f f' t c) : ApproximatesLinearOn f f' s c := fun x hx y hy =>
  hf x (hst hx) y (hst hy)

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