toIsCoatomic

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsStronglyCoatomic.toIsCoatomic

← MathLib Explorer

English

If α is strongly coatomic, then α is coatomic as well.

Русский

Если α сильно коатомно, то α также коатомно.

LaTeX

$$$ IsStronglyCoatomic α \Rightarrow IsCoatomic α $$$

Lean4

instance toIsCoatomic (α : Type*) [PartialOrder α] [OrderTop α] [IsStronglyCoatomic α] : IsCoatomic α :=
  isAtomic_dual_iff_isCoatomic.1 <| IsStronglyAtomic.isAtomic (α := αᵒᵈ)

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

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

Разделы

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

Аффилиация

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