supPrime_iff_not_isMin

Mathlib.Order.Irreducible

URI: https://scilib.ai/kg/mathlib#supPrime_iff_not_isMin

English

In a linear order, SupPrime is equivalent to not being a minimum element.

Русский

В линейном порядке SupPrime эквивалентен тому, что элемент не является минимальным.

LaTeX

$$$\SupPrime a \iff \lnot \IsMin a$$$

Lean4

theorem supPrime_iff_not_isMin : SupPrime a ↔ ¬IsMin a :=
  and_iff_left <| by simp

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

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

Разделы

Аффилиация

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