isCoatomic

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsCoatomic.Set.Ici.isCoatomic

← MathLib Explorer

English

If α is coatomic, then αᵒᵈ is coatomic.

Русский

Если α коатомен, то αᵒᵈ коатомен.

LaTeX

$$$ IsCoatomic α \rightarrow IsCoatomic (OrderDual α) $$$

Lean4

instance isCoatomic {x : α} : IsCoatomic (Set.Ici x) :=
  ⟨fun ⟨y, hy⟩ =>
    (eq_top_or_exists_le_coatom y).imp Subtype.mk_eq_mk.2 fun ⟨a, ha, hay⟩ =>
      ⟨⟨a, le_trans hy hay⟩, ha.Ici (le_trans hy hay), hay⟩⟩

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

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

Разделы

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

Аффилиация

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