isAtomic_dual_iff_isCoatomic

Mathlib.Order.Atoms

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

← MathLib Explorer

English

IsAtomic αᵒᵈ is equivalent to IsCoatomic α, under [OrderTop α].

Русский

IsAtomic αᵒᵈ эквивалентно IsCoatomic α при [OrderTop α].

LaTeX

$$$ IsAtomic (OrderDual\ α) \iff IsCoatomic α $$$

Lean4

@[simp]
theorem isAtomic_dual_iff_isCoatomic [OrderTop α] : IsAtomic αᵒᵈ ↔ IsCoatomic α :=
  ⟨fun h => ⟨fun b => by apply h.eq_bot_or_exists_atom_le⟩, fun h => ⟨fun b => by apply h.eq_top_or_exists_le_coatom⟩⟩

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

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

Разделы

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

Аффилиация

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