not_isMin

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.IsSuccLimit.not_isMin

English

If a is a successor limit, then a is not a minimum.

Русский

Если a является пределом следующего элемента, то он не является минимальным.

LaTeX

$$$IsSuccLimit(a) \rightarrow \neg IsMin(a)$$$

Lean4

protected theorem not_isMin (h : IsSuccLimit a) : ¬IsMin a :=
  h.1

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

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

Разделы

Аффилиация

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