univ_eq

Mathlib.Data.Sign.Basic

URI: https://scilib.ai/kg/mathlib#SignType.univ_eq

English

The range of any function f: SignType → α equals {f(0), f(-1), f(1)}.

Русский

Образ любой функции f: SignType → α равен {f(0), f(-1), f(1)}.

LaTeX

$$$\text{Set.range } f = \{f(0), f(-1), f(1)\}$$$

Lean4

theorem univ_eq : (Finset.univ : Finset SignType) = {0, -1, 1} := by decide

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

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

Разделы

Аффилиация

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