eq_sInf_coatoms

Mathlib.Order.Atoms

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

← MathLib Explorer

English

In a complete lattice that is coatomistic, there exists a set of coatoms whose infimum is b.

Русский

Существет множество коатомов, чье инфимина равняется b.

LaTeX

$$CompleteLattice.isCoatomistic_iff.1 ‹_› b$$

Lean4

theorem eq_sInf_coatoms {α} [CompleteLattice α] [IsCoatomistic α] (b : α) :
    ∃ s : Set α, b = sInf s ∧ ∀ a ∈ s, IsCoatom a :=
  CompleteLattice.isCoatomistic_iff.1 ‹_› b

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

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

Разделы

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

Аффилиация

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