principal

Mathlib.Order.Ideal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.principal

← MathLib Explorer

English

If I is a coatom, then I is maximal.

Русский

Если I коатом, то он максимален.

LaTeX

$$IsCoatom(I) \Rightarrow IsMaximal(I)$$

Lean4

/-- The smallest ideal containing a given element. -/
@[simps]
def principal (p : P) : Ideal P where
  toLowerSet := LowerSet.Iic p
  nonempty' := nonempty_Iic
  directed' _ hx _ hy := ⟨p, le_rfl, hx, hy⟩

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

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

Разделы

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

Аффилиация

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