eq_zero_iff — Mathlib

English

eVariationOn f s equals 0 iff f is constant on s in the metric sense: edist(f x, f y) = 0 for all x,y ∈ s.

Русский

eVariationOn f s = 0 тогда, когда f константен на s по расстоянию edist: edist(f x, f y)=0 для всех x,y ∈ s.

LaTeX

$$$eVariationOn f s = 0 \iff (\forall x\in s)(\forall y\in s), edist(f x, f y) = 0$$

Lean4

theorem eq_zero_iff (f : α → E) {s : Set α} : eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0 :=
  by
  constructor
  · rintro h x xs y ys
    rw [← le_zero_iff, ← h]
    exact edist_le f xs ys
  · rintro h
    dsimp only [eVariationOn]
    rw [ENNReal.iSup_eq_zero]
    rintro ⟨n, u, um, us⟩
    exact Finset.sum_eq_zero fun i _ => h _ (us i.succ) _ (us i)

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