mono_num — Mathlib

English

If s ⊆ t and ApproximatesLinearOn holds on t with constant c, then it also holds on s with the same c.

Русский

Если s ⊆ t и ApproximatesLinearOn выполняется на t с константой c, то оно выполняется и на s с той же константой.

LaTeX

$$$\text{ApproximatesLinearOn}(f,f',s,c) = (s ⊆ t) \rightarrow \text{ApproximatesLinearOn}(f,f',t,c)$$$

Lean4

theorem mono_num (hc : c ≤ c') (hf : ApproximatesLinearOn f f' s c) : ApproximatesLinearOn f f' s c' := fun x hx y hy =>
  le_trans (hf x hx y hy) (mul_le_mul_of_nonneg_right hc <| norm_nonneg _)

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