subsingleton

Mathlib.Topology.EMetricSpace.BoundedVariation

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

English

If s is subsingleton, eVariationOn f s = 0 for any f.

Русский

Если s с subsingleton, то для любой f вариация равна нулю.

LaTeX

$$$s\text{ Subsingleton} \Rightarrow eVariationOn f s = 0$$

Lean4

@[simp]
protected theorem subsingleton (f : α → E) {s : Set α} (hs : s.Subsingleton) : eVariationOn f s = 0 :=
  constant_on (hs.image f)

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

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

Разделы

Аффилиация

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