constant_on

Mathlib.Topology.EMetricSpace.BoundedVariation

URI: https://scilib.ai/kg/mathlib#eVariationOn.constant_on

← MathLib Explorer

English

If the image f''s s is subsingleton, then eVariationOn f s = 0.

Русский

Если образ f на s является одноэлементным, то eVariationOn f s = 0.

LaTeX

$$$\big(f''s).Subsingleton \Rightarrow eVariationOn f s = 0$$

Lean4

theorem constant_on {f : α → E} {s : Set α} (hf : (f '' s).Subsingleton) : eVariationOn f s = 0 :=
  by
  rw [eq_zero_iff]
  rintro x xs y ys
  rw [hf ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩, edist_self]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru