English
HasConstantSpeedOnWith f s 0 is equivalent to edist(f x, f y) = 0 for all x,y in s; i.e., equal values on s.
Русский
HasConstantSpeedOnWith f s 0 эквивалентно edist(f x, f y) = 0 для всех x,y ∈ s; то есть значения совпадают на s.
LaTeX
$$HasConstantSpeedOnWith f s 0 ⇔ ∀ x∈s, ∀ y∈s, edist(f x, f y) = 0$$
Lean4
theorem hasConstantSpeedOnWith_zero_iff : HasConstantSpeedOnWith f s 0 ↔ ∀ᵉ (x ∈ s) (y ∈ s), edist (f x) (f y) = 0 :=
by
dsimp [HasConstantSpeedOnWith]
simp only [zero_mul, ENNReal.ofReal_zero, ← eVariationOn.eq_zero_iff]
constructor
· by_contra!
obtain ⟨h, hfs⟩ := this
simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h
push_neg at hfs
obtain ⟨x, xs, y, ys, hxy⟩ := hfs
rcases le_total x y with (xy | yx)
· exact hxy (h xs ys x ⟨xs, le_rfl, xy⟩ y ⟨ys, xy, le_rfl⟩)
· rw [edist_comm] at hxy
exact hxy (h ys xs y ⟨ys, le_rfl, yx⟩ x ⟨xs, yx, le_rfl⟩)
· rintro h x _ y _
refine le_antisymm ?_ zero_le'
rw [← h]
exact eVariationOn.mono f inter_subset_left
