range_const_subset

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.range_const_subset

English

The range of a constant function is contained in the singleton set containing its value.

Русский

Диапазон константной функции содержится в синглетоне, содержащем её значение.

LaTeX

$$$\\mathrm{const}(\\alpha,b)\\mathrm{.range} \\subseteq \\{ b \\}$$$

Lean4

theorem range_const_subset (α) [MeasurableSpace α] (b : β) : (const α b).range ⊆ { b } :=
  Finset.coe_subset.1 <| by simp

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

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

Разделы

Аффилиация

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