not_isMin

Mathlib.Order.Irreducible

URI: https://scilib.ai/kg/mathlib#SupIrred.not_isMin

English

If an element a is SupIrred, then a is not a minimal element.

Русский

Если элемент a является SupIrred, то он не является минимальным элементом.

LaTeX

$$SupIrred\ a \rightarrow \neg IsMin\ a$$

Lean4

theorem not_isMin (ha : SupIrred a) : ¬IsMin a :=
  ha.1

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

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

Разделы

Аффилиация

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