eq_of_eqOn — Mathlib

English

If f and f' are equal on s (i.e., they coincide on s), then their e-variations on s are equal.

Русский

Если f и f' совпадают на s, то их e-variation на s равны.

LaTeX

$$$\forall f,f',s\,\big(\forall x\in s, f x = f' x\big)\Rightarrow eVariationOn f s = eVariationOn f' s$$

Lean4

theorem eq_of_eqOn {f f' : α → E} {s : Set α} (h : EqOn f f' s) : eVariationOn f s = eVariationOn f' s :=
  eq_of_edist_zero_on fun x xs => by rw [h xs, edist_self]

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