sub_smul_slope_vadd — Mathlib

English

The relation (b−a)•slope f a b +ᵥ f a = f b expresses that moving f a by the slope between a and b recovers f b.

Русский

Соотношение (b−a)•slope f a b +ᵥ f a = f b означает, что при переносе точки f a на величину, равную наклону между a и b, достигается f b.

LaTeX

$$$ (b-a) \\cdot \\operatorname{slope} f a b \; +\\!\\!\\!\\!\\!_{v} f a = f b$$$

Lean4

theorem sub_smul_slope_vadd (f : k → PE) (a b : k) : (b - a) • slope f a b +ᵥ f a = f b := by
  rw [sub_smul_slope, vsub_vadd]

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