to_isAtomic

Mathlib.Order.Atoms.Finite

URI: https://scilib.ai/kg/mathlib#Finite.to_isAtomic

← MathLib Explorer

English

The finite order α with bottom and top is atomic (dual of coatomic).

Русский

Конечный порядок α с нижним и верхним элементами атомарен (правая дуальность к коатомности).

LaTeX

$$$\\text{IsAtomic}(α)$$$

Lean4

instance (priority := 100) to_isAtomic [PartialOrder α] [OrderBot α] [Finite α] : IsAtomic α :=
  isCoatomic_dual_iff_isAtomic.mp Finite.to_isCoatomic

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

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

Разделы

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

Аффилиация

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