isAtom_of_image

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#GaloisCoinsertion.isAtom_of_image

← MathLib Explorer

English

In a GaloisCoinsertion, if IsAtom (l a) then IsAtom a.

Русский

В Galois-коином, если IsAtom(l(a)), то IsAtom(a).

LaTeX

$$$\forall a,\ \mathrm{IsAtom}(\,l(a)\,) \Rightarrow \mathrm{IsAtom}(a)$$$

Lean4

theorem isAtom_of_image [OrderBot α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) {a : α}
    (hb : IsAtom (l a)) : IsAtom a :=
  gi.dual.isCoatom_of_image hb.dual

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

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

Разделы

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

Аффилиация

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