empty

Mathlib.Logic.Function.DependsOn

URI: https://scilib.ai/kg/mathlib#DependsOn.empty

English

A function depending on the empty set is constant.

Русский

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

LaTeX

$$$\forall f\,\big(DependsOn f \emptyset\big) \to \forall x,y:\; f(x)=f(y)$$$

Lean4

/-- A function which depends on the empty set is constant. -/
theorem empty (hf : DependsOn f ∅) (x y : Π i, α i) : f x = f y :=
  hf (by simp)

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

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

Разделы

Аффилиация

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