eq_of_edist_zero_on — Mathlib

English

If two functions f and f' have zero distance pointwise on a set s, then their e-variation on s coincides: eVariationOn(f, s) = eVariationOn(f', s).

Русский

Если две функции f и f' удовлетворяют условию edist(f x, f'(x)) = 0 для всех x ∈ s, то их e-variation на s совпадает: eVariationOn(f, s) = eVariationOn(f', s).

LaTeX

$$$\forall f,f',s\left(\forall x\,(x\in s \rightarrow \operatorname{edist}(f x,f' x)=0)\right)\Rightarrow eVariationOn f s = eVariationOn f' s$$

Lean4

theorem eq_of_edist_zero_on {f f' : α → E} {s : Set α} (h : ∀ ⦃x⦄, x ∈ s → edist (f x) (f' x) = 0) :
    eVariationOn f s = eVariationOn f' s := by
  dsimp only [eVariationOn]
  congr 1 with p : 1
  congr 1 with i : 1
  rw [edist_congr_right (h <| p.snd.prop.2 (i + 1)), edist_congr_left (h <| p.snd.prop.2 i)]

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