not_isMin

Mathlib.Order.Irreducible

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

English

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

Русский

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

LaTeX

$$SupPrime\ a \rightarrow \neg IsMin\ a$$

Lean4

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

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

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

Разделы

Аффилиация

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