instIsCoatomistic

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#OrderDual.instIsCoatomistic

English

If α has OrderBot and IsAtomistic, then αᵒᵈ is IsCoatomistic.

Русский

Если у α есть OrderBot и IsAtomistic, то αᵒᵈ коатомистичен.

LaTeX

$$$[OrderBot(\\alpha)] [\\mathrm{IsAtomistic}(\\alpha)] \\Rightarrow \\mathrm{IsCoatomistic}(\\alpha^\\mathrm{op})$$$

Lean4

instance _root_.OrderDual.instIsCoatomistic [OrderBot α] [h : IsAtomistic α] : IsCoatomistic αᵒᵈ :=
  isCoatomistic_dual_iff_isAtomistic.2 h

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

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

Разделы

Аффилиация

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