range_eq

Mathlib.Data.Sign.Basic

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

← MathLib Explorer

English

For any function f, Set.range f equals the three-element set {f(0), f(-1), f(1)}.

Русский

Для любой функции f множество образа равняется тройке {f(0), f(-1), f(1)}.

LaTeX

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

Lean4

theorem range_eq {α} (f : SignType → α) : Set.range f = {f zero, f neg, f pos} :=
  by
  classical rw [← Fintype.coe_image_univ, univ_eq]
  classical simp [Finset.coe_insert]

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

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

Разделы

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

Аффилиация

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