findAtom_ne_bot

Mathlib.Order.SuccPred.Tree

URI: https://scilib.ai/kg/mathlib#IsPredArchimedean.findAtom_ne_bot

English

If r ≠ ⊥, then findAtom r is an atom.

Русский

Если r ≠ ⊥, то findAtom r является атомом.

LaTeX

$$IsAtom(findAtom r), \\text{ for } r ≠ ⊥$$

Lean4

theorem findAtom_ne_bot {r : α} : findAtom r ≠ ⊥ ↔ r ≠ ⊥ :=
  findAtom_eq_bot.not

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

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

Разделы

Аффилиация

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