range_some_union_none

Mathlib.Data.Set.Image

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

English

The union of the range of some with { none } is the universal set.

Русский

Объединение диапазона some и { none } даёт все множество.

LaTeX

$$$$ \\operatorname{range}(\\text{some}) \\cup \\{ \\text{none} \\} = \\operatorname{univ} $$$$

Lean4

theorem range_some_union_none (α : Type*) : range (some : α → Option α) ∪ { none } = univ :=
  (isCompl_range_some_none α).sup_eq_top

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

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

Разделы

Аффилиация

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