range_single_subset

Mathlib.Data.Finsupp.Single

URI: https://scilib.ai/kg/mathlib#Finsupp.range_single_subset

English

Every value in the range of single a b lies in {0, b}.

Русский

Любое значение в образе функции single a b лежит в {0, b}.

LaTeX

$$$$\\operatorname{range}(\\text{single } a\\, b) \\subseteq \\{0, b\\}.$$$$

Lean4

theorem range_single_subset : Set.range (single a b) ⊆ {0, b} :=
  Set.range_subset_iff.2 single_apply_mem

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

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

Разделы

Аффилиация

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