eq_none_or_eq_some

Mathlib.Data.Part

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

English

Every Part is either none or some x for some x; i.e., o = none or ∃ x, o = some x.

Русский

Каждая часть либо none, либо существует x, такая что o = some x.

LaTeX

$$$$\forall o:\mathrm{Part}\,\alpha,\; o = \mathrm{none} \;\lor\; \exists x, o = \mathrm{some}(x). $$$$

Lean4

theorem eq_none_or_eq_some (o : Part α) : o = none ∨ ∃ x, o = some x :=
  or_iff_not_imp_left.2 ne_none_iff.1

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

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

Разделы

Аффилиация

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