range_const

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.range_const

English

If the index type is nonempty, the range of a constant map is the singleton {c}.

Русский

Если базовый тип непуст, образ константного отображения равен {c}.

LaTeX

$$$\forall [\mathcal{I} \neq \varnothing], \operatorname{range}(\lambda _ : \mathcal{I}, c) = \{ c \}$$$

Lean4

@[simp]
theorem range_const : ∀ [Nonempty ι] {c : α}, (range fun _ : ι => c) = { c } :=
  range_eq_singleton (fun _ => rfl)

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

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

Разделы

Аффилиация

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