InfIrred

Mathlib.Order.Irreducible

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

Lean4

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

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

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

Разделы

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

Аффилиация

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