none_toOption

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.none_toOption

English

The toOption of none is the empty option: (none : Part α).toOption = Option.none.

Русский

toOption для none равен пустому варианту: (none : Part α).toOption = Option.none.

LaTeX

$$$ (\mathrm{none} : \mathrm{Part}(\alpha)).\\mathrm{toOption} = \\mathrm{Option.none} $$$

Lean4

@[simp]
theorem none_toOption [Decidable (@none α).Dom] : (none : Part α).toOption = Option.none :=
  dif_neg id

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

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

Разделы

Аффилиация

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