not_none_dom

Mathlib.Data.Part

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

English

The domain of none is false; i.e., not (none).Dom.

Русский

Область определения none ложно; то есть ¬(none).Dom.

LaTeX

$$$$\neg (\text{none} : \mathrm{Part}\,\alpha).\Dom.$$$$

Lean4

@[simp]
theorem not_none_dom : ¬(none : Part α).Dom :=
  id

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

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

Разделы

Аффилиация

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