some_ne_none

Mathlib.Data.Part

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

English

Some x is never equal to none; i.e., some x ≠ none.

Русский

some x никогда не равно none; то есть some x ≠ none.

LaTeX

$$$$\forall x:\alpha,\; \mathrm{some}(x) \neq \mathrm{none}.$$$$

Lean4

@[simp]
theorem some_ne_none (x : α) : some x ≠ none := by
  intro h
  exact true_ne_false (congr_arg Dom h)

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

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

Разделы

Аффилиация

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