range_eq_empty

Mathlib.Data.Set.Image

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

English

range f = ∅ when ι is empty.

Русский

Диапазон f пуст, если ι пуст.

LaTeX

$$$ \\text{[IsEmpty } ι] \\to \\operatorname{range} f = \\emptyset$$$

Lean4

theorem range_eq_empty [IsEmpty ι] (f : ι → α) : range f = ∅ :=
  range_eq_empty_iff.2 ‹_›

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

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

Разделы

Аффилиация

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