dependsOn_const

Mathlib.Logic.Function.DependsOn

URI: https://scilib.ai/kg/mathlib#dependsOn_const

← MathLib Explorer

English

A function that depends on the empty set is constant.

Русский

Функция, зависящая от пустого множества, константна.

LaTeX

$$$DependsOn(\lambda _ : \Pi i, α i, b)\, \emptyset$$$

Lean4

/-- A constant function does not depend on any variable. -/
theorem dependsOn_const (b : β) : DependsOn (fun _ : Π i, α i ↦ b) ∅ := by simp [DependsOn]

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

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

Разделы

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

Аффилиация

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