InfPrime

Mathlib.Order.Irreducible

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

Lean4

/-- An inf-prime element is a non-top element which isn't bigger than the infimum of anything
bigger. -/
def InfPrime (a : α) : Prop :=
  ¬IsMax a ∧ ∀ ⦃b c⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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